PDF de programación - Tema 0 - Tecnología de la Programación

UNIVERSIDAD DE A CORUÑA
FACULTAD DE INFORMÁTICA

DEPARTAMENTO DE COMPUTACIÓN

Tema 0: Prólogo

Tecnología de la Programación

Ingeniería Técnica en Informática de Sistemas

Elena Mª Hernández Pereira

Óscar Fontenla Romero

 Tecnología de la programación:

 Técnicas de verificación y pruebas de programas

Descriptor B.O.E.

 Análisis de algoritmos Descriptor B.O.E.

 Secuencia desarrollo programa

 Especificar: Describir lo que debe hacer un programa
 Implementar: Combinar instrucciones de un lenguaje

de programación para realizar una función

 Verificar: Comprobar si un programa si funciona o no

⇒ cumple con las especificaciones

Tecnología de la programación - Elena Hernández & Oscar Fontenla

2

Tema 0: Prólogo

Tema 0: Prólogo

o Verificación a posteriori

• Comprobar mediante trazas de ejecución
• Utilizar herramientas de depuración

o Verificación a priori

• Demostrar la corrección de modo formal

o Especificación

• Declarativa, precisa y breve
• Utilizando lenguaje formal ⇒ Especificación

formal

o Antony Hoare

• 1962, creador del QuickSort
• 1969, Programación estructurada
 Desarrollo de la lógica de Hoare

o Dijkstra

• 1976, A discipline of Programming: verificación formal, weakest

precondition, derivación de programas

o Lógica de Hoare

• Especificación y verificación formal
• Objetivo: demostración lógica de la corrección de un programa

o ¿Por qué utilizar la lógica? ¿Por qué probar que un

programa es correcto?

Tecnología de la programación - Elena Hernández & Oscar Fontenla

3

Tecnología de la programación - Elena Hernández & Oscar Fontenla

4

Tema 0: Prólogo

Tema 0: Prólogo

o Ejemplo de la importancia

de especificar bien:
• Calcular el resto r y el cociente

c de dividir un entero no
negativo x entre un entero
positivo y

• No disponemos de la operación

división entera

...
r := x;
c := 0;
while r > y do

begin

r := r – y;
c := c + 1;

end;

...

Divisor mayor que cero
Al terminar x = y*c +r

o Incluimos write

o Solución que produce

demasiada salida

...
write(‘dividendo x =‘,x);
write(‘divisor y =‘,y);
r := x;
c := 0;
while r > y do

begin

r := r – y;
c := c + 1;

end;

write(‘y *c + r =‘,y*c+r);
...

Tecnología de la programación - Elena Hernández & Oscar Fontenla

5

Tecnología de la programación - Elena Hernández & Oscar Fontenla

6

1

Tema 0: Prólogo

Tema 0: Prólogo

o Aserciones

o Expresión booleana

entre llaves

o Se vuelcan valores si

estos son falsos

o Supongamos:

o x=6, y=3, c=1 y r=3

...
{y > 0}
r := x;
c := 0;
while r > y do

begin

r := r – y;
c := c + 1;

end;

{x = y *c + r}
...

o El resto debe ser

menor que el divisor
o Modificamos la

condición del bucle

o Al final r < y

...
{y > 0}
r := x;
c := 0;
while r ≥ y do

begin

r := r – y;
c := c + 1;

end;

o ¿Qué pasa si r = -2 ?

{x = y *c + r and r < y}
...

Tecnología de la programación - Elena Hernández & Oscar Fontenla

7

Tecnología de la programación - Elena Hernández & Oscar Fontenla

8

Tema 0: Prólogo

Tema 0: Prólogo

o El cociente debe ser

inicialmente mayor que
cero
o Modificamos la aserción

inicial

o Necesitamos una

aproximación
sistemática para probar
la corrección de un
programa

...
{y > 0 and x ≥ 0}
r := x;
c := 0;
while r ≥ y do

begin

r := r – y;
c := c + 1;

end;

{x = y *c + r and r < y}
...

o Corrección

• Mantener propiedades deseables de un

programa

o Propiedades de programas secuenciales

• Corrección parcial
 Resultado correcto
 No hay garantía de finalización

• Terminación
• Ausencia de fallos

Tecnología de la programación - Elena Hernández & Oscar Fontenla

9

Tecnología de la programación - Elena Hernández & Oscar Fontenla

10

2