PDF de programación - Semántica Axiomática - Tecnología de la Programación

Tecnología de la Programación

Semántica Axiomática

David Cabrero Souto

Facultad de Informática
Universidade da Coruña

Curso 2007/2008

Semántica Axiomática

Busca demostrar la corrección de un programa respecto a
una especificación.
Especificación = precondición y postcondición
(Diseño por contrato)
C.A.R. Hoare

Quicksort, Lógica de Hoare, Communicating Sequential
Processes

Lógica de Hoare

Paper “An axiomatic basis for computer programming”, 1969.
Reglas lógicas para razonar sobre la corrección de programas

Triple de Hoare

{P} S {Q}
El triple es válido si

siempre que la ejecución del programa S comienza
en un estado σ que satisface P, entonces termina en
un estado σ que satisface Q

P Precondición, Q Postcondición
Si el triple {P} S {Q} es válido, entonces el programa S es
correcto respecto a la especificación

Ejemplos

Triples válidos

{ i = 0 }

i := i + 1;

{ i = 1 }

{ i+j = 0 }

i := i + 1;
j := j -1 ;

{ i+j = 0}

{ true }

i := 1;

{ i = 1}

Triples no válidos
{ i = 1}

i := i + 1;

{ i = 0}

{ i+j <> 0 }

i := i +1;
j := j -1;

{ i+j = 0 }

{ true }

i := 1;

{ i = 0 }

Corrección parcial vs. total

Corrección parcial
Si termina, el programa es correcto respecto a la
especificación
Corrección total
El programa termina y es correcto respecto a la
especificación
Ejemplo: {A} c {B}
c ≡ while true do skip done
Es inmediato demostrar la corrección parcial, pero no es
posible demostrar la corrección total
La Lógica de Hoare (original) sólo prueba la corrección
parcial

Reglas de Hoare para corrección parcial
Axiomas

Skip

Asignación

{A} skip; {A}

{A[a/X ]} X := a; {A}

Ejemplo

{P} i := 2*i; {i < 10}
Calcular la precondición

1 Aplicamos el axioma de la asignación

{i < 10[2 ∗ i/i]} i := 2*i; {i < 10}

2 Simplificamos

3 Simplificamos

{2 ∗ i < 10} i := 2*i; {i < 10}

{i < 5} i := 2*i; {i < 10}

Reglas de Hoare para corrección parcial
Regla de secuencia

Secuencia

{A} c0; {C}

{A}

c0; c1

{C} c1 {B}

{B}

Ejemplo (I)

Swap de X e Y:
{X = n ∧ Y = m}

Z := X;
X := Y;
Y := Z;

{X = m ∧ Y = n}

¿ Es correcto ?

1 Axioma asignación

{X = n ∧ Y = m}
{Z = n ∧ Y = m}

Z := X;

2 Axioma asignación

{Z = n ∧ Y = m}
{Z = n ∧ X = m}

X := Y;

3 Regla de secuencia (1 y 2)

{X = n ∧ Y = m}

Z := X;
X := Y;

{Z = n ∧ X = m}

Ejemplo (II)

4 Axioma asignación

{Z = n ∧ X = m}
{Y = n ∧ X = m}

Y := Z;

5 Regla de secuencia (3 y 4)
{X = n ∧ Y = m}

Z := X;
X := Y;
Y := Z;

{Y = n ∧ X = m}

6 q.e.d.

Reglas de Hoare para corrección parcial
Regla del condicional

Condicional

{A ∧ b} c0; {B}

{A ∧ ¬b} c1 {B}

{A} if b then c0 else c1 fi {B}

La instrucción es no determinista (b ∨ ¬b)
Se verifican ambas alternativas

Ejemplo: if (I)

Valor absoluto de X:
{true}

if (X <= 0) then

Y := -X;

else

fi

Y := X;
{Y = |X|}
¿ Es correcto ?

{true ∧ X ≤ 0} Y := -X; {Y = |X|} {true ∧ ¬X ≤ 0} Y := X; {Y = |X|}

{true} if (X <= 0) then ...fi {Y = |X|}

Notación alternativa

Intercalar condiciones en el código.
{true}

if (X <= 0) then

{true ∧ X ≤ 0} Y := -X; {Y = |X|}
{true ∧ ¬X ≤ 0} Y := X; {Y = |X|}

else

fi

{Y = |X|}

Ejemplo: if (II)

Primera premisa: {true ∧ X ≤ 0} Y := -X; {Y = |X|}
1 Regla de asignación para {P} Y := -X; {Y = |X|}:

{−X = |X|} Y := -X; {Y = |X|}

Segunda premisa: {true ∧ ¬X ≤ 0} Y := -X; {Y = |X|}
1 Regla de asignación para {P} Y := -X; {Y = |X|}:

{X = |X|} Y := -X; {Y = |X|}

Necesitamos una nueva regla para continuar.

Reglas de Hoare para corrección parcial
Regla de la implicación

Implicación

|= (A ⇒ A)

{A} c {B}
{A}
{B}

c

|= (B ⇒ B)

Ejemplo: if (III)

Primera premisa

2 Por la definición de valor absoluto:
{true ∧ X ≤ 0} ⇒ {−X = |X|}

3 Regla de la implicación (1 y 2)

{true ∧ X ≤ 0} Y := -X; {Y = |X|}

Segunda premisa

2 Por la definición de valor absoluto:
{true ∧ ¬X ≤ 0} ⇒ {X = |X|}

3 Regla de la implicación (1 y 2)

{true ∧ ¬X ≤ 0} Y := X; {Y = |X|}

q.e.d.

Reglas de Hoare para corrección parcial
Regla del while

While

{A ∧ b} c {A}

{A} while b do c done {A ∧ ¬b}

A es la invariante del bucle

Ejemplo: while (I)

Cálculo del factorial de n

{X = n ∧ n ≥ 0 ∧ Y = 1}

while X>0 do
Y := Y * X;
X := X - 1;

done
{Y = n!}

Invariante

I ≡ Y ∗ X ! = n! ∧ X ≥ 0

¿ Es correcto ?

{I ∧ X > 0} c {I}

{I} while X>0 do c done {I ∧ ¬X > 0}
c ≡ Y := Y * X; X := X - 1;

Ejemplo: while (II)

La invariante es: I ≡ Y ∗ X ! = n! ∧ X ≥ 0
Comprobamos la premisa: {I ∧ X > 0} c {I}
1 Axioma de asignación

{Y ∗ (X − 1)! = n! ∧ (X − 1) ≥ 0}
{I} ≡ {Y ∗ X ! = n! ∧ X ≥ 0}

X := X - 1;

2 Axioma de asignación

{Y ∗ X ∗ (X − 1)! = n! ∧ (X − 1) ≥ 0}
{Y ∗ (X − 1)! = n! ∧ (X − 1) ≥ 0}

Y := Y - X;

3 Regla de la secuencia (1 y 2)

{Y ∗ X ∗ (X − 1)! = n! ∧ (X − 1) ≥ 0}

Y := Y * X;
X := X - 1;

{I} ≡ {Y ∗ X ! = n! ∧ X ≥ 0}

Ejemplo: while (III)

4 Por la definición de factorial

{Y ∗ X ∗ (X − 1)! = n! ∧ (X − 1) ≥ 0} ≡
{Y ∗ X ! = n! ∧ (X − 1) ≥ 0}

5 Y

{Y ∗ X ! = n! ∧ (X − 1) ≥ 0} ≡ {Y ∗ X ! = n! ∧ X > 0}
{Y ∗ X ! = n! ∧ X > 0} ⇒ {I ∧ X > 0}

6 Regla de la implicación (3 y 5)

{I ∧ X > 0}
Y := Y * X;
X := X - 1;

{I}

7 Regla del while (6)

{I}
{I ∧ ¬X > 0} ≡ {I ∧ X ≤ 0}

while X>0 do c done

Ejemplo: while (IV)

8 Desarrollamos {I ∧ X ≤ 0}

{I ∧ X ≤ 0} ≡
{Y ∗ X ! = n! ∧ X ≥ 0 ∧ X ≤ 0} ⇒
{Y ∗ X ! = n! ∧ X = 0} ⇒
{Y = n!}

9 Trabajando sobre la precondición
Y = 1 ⇒ Y ∗ X ! = n!

y por tanto

{X = n ∧ n ≥ 0 ∧ Y = 1} ⇒ {Y ∗ X ! = n! ∧ n ≥ 0}

10 Regla de la implicación (7, 8 y 9)
{X = n ∧ n ≥ 0 ∧ Y = 1}
{Y = n!

while X>0 do c done