PDF de programación - TEMA 6.- VERIFICACION DE PROGRAMAS IMPERATIVOS

TEMA 6.- VERIFICACION DE PROGRAMAS IMPERATIVOS

6.1.- Lógica de Hoare.

Desarrollada por C.A.R. Hoare (1969), es una lógica que permite probar la
verdad o falsedad de propiedades de programas imperativos (especialmente
corrección y terminación) sin concurrencia o paralelismo.

Basada en la idea de diagrama de flujo anotado.

P

Q

S

• S es una “frase” de código en un programa de alto nivel, con una única

entrada y una única salida normal.

◦ Instrucción.
◦ Bloque de instrucciones consecutivas.
◦ Un programa o subprograma.

• Cada frase S denota una relación entre dos estados en un espacio
de estados definido por el producto cartesiano de los valores de las
variables del programa. Es decir, al ejecutar una instrucción o secuencia de
instrucciones S, se modifica el valor de una o varias variables, transitando
de un estado a otro.

• P y Q son anotaciones, fórmulas de la Lógica de Primer Orden (Lógica

de Predicados).

◦ P ≡ Precondición (se refiere al estado previo a S)
◦ Q ≡ Postcondición (se refiere al estado posterior a S)

Notación : {P }S{Q}

Significado:

• Corrección parcial: si la precondición P es cierta antes de ejecutar la frase
de programa S, y la ejecución termina normalmente, la postcondición Q
es cierta.

|=par {P }S{Q}

• Corrección total: si la precondición P es cierta antes de la ejecución de la

frase de programa S, esta termina y la postcondición Q es cierta.

|=tot {P }S{Q}

1

En la corrección parcial, la frase S debe terminar normalmente. Existen dos
posibles fuentes de terminación anormal:

• Bucle infinito.
• Error de ejecución (división entre cero, overflow, . . . ).

Correccion total implica corrección parcial. Sin embargo, en muchas ocasiones
se demuestra primero la segunda y, a partir de ella la primera.

En Lógica de Hoare se utilizan dos lenguajes formales:

• Un lenguaje de programación imperativo (LP) para S.
• Un lenguaje de fórmula (LF) para P y Q. En LF se usan los tipos (enteros,
booleanos, reales, . . . ), funciones (suma de enteros, suma de reales...) y
predicados(<, >, ≤, . . . ) usados en el LP, incluídos los definidos por el
usuario.

Para hacer pruebas sobre Lógica de Hoare presentaremos un método de
prueba sintáctico. Primero veremos como demostrar si una tripla {P }S{Q}
es derivable para la condición de corrección parcial

y después presentaremos las condiciones necesarias para tener corrección total.

⊢par {P }S{Q}

⊢tot {P }S{Q}

Puede demostrarse (aunque no lo haremos, podeis respirad tranquilos) la
coherencia de las pruebas, mientras que la complección se cumplirá sólo en
determinadas circunstancias, tanto con corrección parcial como total.

coherencia

⊢par {P }S{Q} ⇒ |=par {P }S{Q}

compleccion |=par {P }S{Q} ; ⊢par {P }S{Q}

Sea S un programa y P su precondición, {P }S{F also} significa que S nunca
termina cuando se comienza en P . Se trata de un problema indecidible (no se
puede demostrar siempre), de modo que la lógica de Hoare no es completa.

2

6.1.1.- Reglas para la corrección parcial.

Asignación:

{P [E/x]} x = E {P }

• Si el estado inicial es s, entonces el estado s′ después de la asignación es

igual a s, sustituyendo la variable x por el resultado de evaluar E.

• Si s′ satisface P (la hace cierta), la fórmula que satisfará s será P [E/x],
el resultado de sustituír todas las ocurrencias libres de x en P por E.
Ejs.- {y + 5 = 10} y = y + 5 {y = 10}

{y + y < z} x = y {x + y < z}
{2 ∗ (y + 5) > 20} y = 2 ∗ (y + 5) {y > 20}

Composición:

{P }S1{Q} {Q}S2{R}

{P }S1; S2{R}

Aplica la transitividad sobre dos frases para poder obtener la pre y
postcondiciones de la concatenación de ambas.

Instrucción if:

{P ∧ B}S1{Q} {P ∧qB}S2{Q}

{P }if B then S1 else S2{Q}

• Si ambos bloques S1 y S2 tienen la misma postcondición Q, mientras que
la conjunción de la fórmula P con la condición B y, respectivamente, con
su negación qB, son sus precondiciones, P aparece como precondición de
la bifurcación y Q como su postcondición.

• Las condiciones del LP (normalmente expresiones booleanas) deben ser
importadas como parte de las fórmulas lógicas de las anotaciones (en este
caso precondiciones).

While parcial:

{P ∧ B}S{P }

{P }while B do S{P ∧qB}

• Se trata de la regla que permite calcular las pre y post condiciones de un

bucle while satisfaciendo la propiedad de corrección parcial.

• Si la conjunción de las condiciones P y B es la precondición de S y P es su
postcondición, quiere decir que cuando P y B son ciertas, P será cierto tras
la ejecución de S. Por lo tanto, si B es la ondición del bucle while podemos
demostrar que, siendo cierta la precondición P , se cumple la postcondición
P ∧qB, dado que P era postcondición de la(s) instruccion(es) S del interior
del bucle y qB debe cumplirse para salir del while.

3

Reforzamiento de la precondición (implicación izda.):

R → P {P }S{Q}

{R}S{Q}

• Esta regla permite asumir una precondición más fuerte que la existente,
de ser necesario, sin perder la corrección de la demostración del programa
anotado.

• Permite importar pruebas de la lógica de predicados (concretamente

R → P ).

Debilitamiento de la postcondición (implicación dcha.):

{P }S{Q} Q → R

{P }S{R}

• Esta regla permite asumir una postcondición más débil que la existente,
de ser necesario, sin perder la corrección de la demostración del programa
anotado.

• Permite importar pruebas de la lógica de predicados (concretamente

Q → R).

Otras:

(conjunción)

{P }S{Q1} {P }S{Q2}

{P }S{Q1 ∧ Q2}

(disyunción)

{P1}S{Q} {P2}S{Q}

{P1 ∨ P2}S{Q}

conjunción

inversa {P }S{Q1 ∧ Q2}

{P }S{Qi}

disyunción

inversa {P1 ∨ P2}S{Q}

{Pi}S{Q}

i ∈ {1, 2}

6.1.2.- Corrección parcial.

Partiendo de una especificación (una postcondición y posiblemente alguna
precondición), se trata de demostrar, utilizando las reglas anteriores (y algunas
otras que no hemos visto) que el programa verifica dicha especificación.

Generalmente, tras unas pocas líneas de código, la prueba se hace demasiado
compleja para poder representarla en forma de inferencias encadenadas. Para
resolver este problema se intercalan las anotaciones del LF entre las líneas del
LP.

Dado S ≡ S1; S2; . . . ; Sn, si queremos demostrar que {P0}S{Pn}, basta
demostrar que:

{P0}S1{P1} {P1}S2{P2}

. . .

{Pn−1}Sn{Pn}

4

y usar la regla de la composición n − 1 veces.
De este modo, podemos representar la prueba de {P0}S{Pn} como:

anotación

anotación

{P0}
S1
{P1}
S2
. . .
{Pn−1} anotación
Sn
{Pn}

anotación

Las fórmulas P1, . . . , Pn−1 serán condiciones intermedias y cada paso

{Pi−1}
Si
{Pi}

será obtenido a través de alguna de las reglas anteriores.

El proceso de prueba para un bloque o programa S ≡ S1; S2; . . . ; Sn se produce
de abajo a arriba (desde el fin hacia el principio del bloque o programa) debido
a la naturaleza de la regla de la asignación. En general, comenzamos con la
postcondición Pn y se utiliza Sn para obtener Pn−1.

Obtener Pi−1 a partir de Pi y Si es mecánico para las asignaciones y las
instrucciones if. La Pi−1 obtenida de esa manera se denomina la precondición
más débil para Si y Pi, lo que quiere decir que que Pi−1 es la fórmula lógica
más débil que siendo verdadera al principio de la ejecución de Si garantiza la
veracidad de la postcondición Pi.

0 al principio de la secuencia, que
Al final del proceso, obtenemos una fórmula P ′
garantiza que al ejecutar S se verifica la postcondición Pn. Debemos chequear
si P ′
0 puede obtenerse a partir de la precondición P0 mediante la regla de
reforzamiento de la precondición.
En este caso, deberíamos demostrar que P0 → P ′
0, usando cualquiera de
los sistemas deductivos de lógica de predicados. En general, ese tipo de
demostraciones, que aparecen al usar las dos reglas de la implicación, suelen
omitirse en la secuencia de anotaciones e instrucciones. Si se demuestra que
P → R, la práctica habitual es simplemente escribir la segunda condición
debajo de la primera.

{P }
{R}
S
{Q}

5

Para la calcular la precondición más débil P para un if a partir de una
prostcondición Q

{P } if B then S1 else S2 {Q}

suele precederse del siguiente modo:

1. Se obtiene la precondición P1 a partir de Q y S1.
2. Se obtiene la precondición P2 a partir de Q y S2.
3. P ≡ (B → P1) ∧ (qB → P2)

Recordemos el while parcial:

{P ∧ B}S{P }

{P }while B do S{P ∧qB}

Si tenemos una precondición R y una postcondición Q, y queremos demostrar:

|=par {R}while B do S{Q}

Debemos encontrar una fórmula P del LF que verifique:

1. R → P (para el reforzamiento de la precondición)
2. P ∧qB → Q (para el debilitamiento de la postcondición)
3. |=par {P }while B do S{P ∧qB} (regla while parcial)

A la fórmula P verificando lo anterior se le denomina invariante.

Encontrar invariantes requiere cierto ingenio (puede haber muchas diferentes
para un mismo bucle), aunque hay reglas heurísticas:

1. Comenzar modificando la postcondición del while para hacerla
dependiente del índice del bucle (la variable que crece o decrece en cada
iteración).

2. Si la invariante P aún no verifica P ∧qB → Q, debemos reforzar P para

que se cumpla.

6.1.3.- Corrección total.

Lo anterior sólo prueba la corrección parcial de las triplas {P }S{Q}, es decir,
sólo es cierto cuando S termina normalmente.

Habíamos visto dos posibles razones para la no terminación: error de ejecución
y bucle infinito. La primera está cubierta por el sistema de cálculo que ya
hemos descrito.

6

Por lo tanto, asegurar la corrección total implica asegurar la corrección parcial
y la terminación de los bucles while.

Podemos obtener la prueba de terminación si podemos, a partir de las variables
de los estados del bucle, encontrar una expresión entera que disminuya en cada
iteración del bucle manteniéndose no negativa (0 o positiva).

Si tal expresión existe, en bucle termina después de un número finito de
iteraciones, ya que no hay cadenas descendentes i