Teórica04

Vista previa del material en texto

Precondición más débil
Algoritmos y Estructuras de Datos I
1
Repaso: Corrección de un programa
I Definición. Decimos que un programa S es correcto respecto
de una especificación dada por una precondición P y una
postcondición Q, si siempre que el programa comienza en un
estado que cumple P,
I el programa termina su ejecución,
I y en el estado final se cumple Q.
I Notación. Cuando S es correcto respecto de la especificación
(P,Q), lo denotamos con la siguiente tripla de Hoare:
{P} S {Q}.
2
Repaso: Un lenguaje imperativo simplificado
I Para facilitar nuestro trabajo, definimos un lenguaje
imperativo sencillo, al que llamamos SmallLang.
I SmallLang únicamente soporta las siguientes instrucciones:
1. Asignación: Instrucción x := E.
2. Nada: Instrucción skip que no hace nada.
I Además, soporta las siguientes estructuras de control:
1. Secuencia: S1; S2 es un programa, si S1 y S2 son dos
programas.
2. Condicional: if B then S1 else S2 endif es un programa, si B
es una expresión lógica y S1 y S2 son dos programas.
3. Ciclo: while B do S endwhile es un programa, si B es una
expresión lógica y S es un programa.
3
Demostrando que un programa es correcto
I Sabemos razonar sobre la corrección de nuestros programas,
anotando el código con predicados que representan los
estados.
I Nos interesa formalizar estos razonamientos, para estar
seguros de que no cometimos errores en la demostración.
I Una forma de conseguirlo es la siguiente: A partir de la tripla
de Hoare {P} S {Q}, obtener una fórmula lógica α tal que
α es verdadera si y sólo si {P} S {Q} es verdadera.
I Entre otras cosas, esto nos permite automatizar la
demostración con un verificador automático (!)
4
Demostraciones de corrección
I Buscamos un mecanismo para demostrar “automáticamente”
la corrección de un programa respecto de una especificación
(es decir, la validez de una tripla de Hoare).
I ¿Es válida esta tripla?
{x ≥ 4}
x := x + 1
{x ≥ 7}
I No. Contrajemplo: con x = 4 no se cumple la postcondición.
I ¿Es válida esta tripla?
{x ≥ 4}
x := x + 1
{x ≥ 5}
I Śı. Es válida!
5
Precondición más débil
I Definición. La precondición más débil de un programa S
respecto de una postcondición Q es el predicado P más débil
posible tal que {P}S{Q}.
I Notación. wp(S,Q).
I Teorema: Una tripla de Hoare {P}S{Q} es válida si y sólo si:
P ⇒L wp(S ,Q)
6
Precondición más débil
I Ejemplo:
{wp(x := x+1,Q)}
x := x + 1
{Q : x ≥ 7}
I ¿Cuál es la precondición más débil de x:=x+1 con respecto a
la postcondición x ≥ 7?
I wp(x := x+1,Q)) ≡ x ≥ 6.
7
Precondición más débil
I Otro ejemplo:
{wp(S2,Q)}
S2: x := 2 * |x| + 1
{Q : x ≥ 5}
I wp(S2,Q) ≡ x ≥ 2 ∨ x ≤ −2.
I Otro más:
{wp(S3,Q)}
S3: x := y*y
{Q : x ≥ 0}
I wp(S3,Q) ≡ True.
8
Precondición más débil
I Si para demostrar la validez de {P}S{Q} nos alcanza con
probar la fórmula:
P ⇒L wp(S ,Q)
I Entonces lo que necesitamos un mecanismo para obtener la
wp de (S,Q).
I Afortunadamente, existe un conjunto de axiomas que
podemos usar para obtener la wp
I Antes de empezar a ver estos axiomas, definamos primero dos
predicados: def (E ) y QxE
9
Predicado def(E)
I Definición. Dada una expresión E , llamamos def(E ) a las
condiciones necesarias para que E esté definida.
1. def(x + y) ≡ def(x) ∧ def(y).
2. def(x/y) ≡ def(x) ∧ (def(y) ∧L y 6= 0).
3. def(
√
x) ≡ def(x) ∧L x ≥ 0.
4. def(a[i ] + 3) ≡ (def(a) ∧ def(i)) ∧L 0 ≤ i < |a|.
I Suponemos def(x) ≡ True para todas las variables, para
simplificar la notación.
I Con esta hipótesis extra:
1. def(x + y) ≡ True.
2. def(x/y) ≡ y 6= 0.
3. def(
√
x) ≡ x ≥ 0.
4. def(a[i ] + 3) ≡ 0 ≤ i < |a|.
10
Predicado QxE
I Definición. Dado un predicado Q, el predicado QxE se obtiene
reemplazando en Q todas las apariciones libres de la variable
x por E .
1. Q ≡ 0 ≤ i < j < n ∧L a[i ] ≤ x < a[j ].
Q ik ≡ 0 ≤ k < j < n ∧L a[k] ≤ x < a[j ].
Q ii+1 ≡ 0 ≤ i + 1 < j < n ∧L a[i + 1] ≤ x < a[j ].
2. Q ≡ 0 ≤ i < n ∧L (∀j : Z)(a[j ] = x).
Q jk ≡ 0 ≤ i < n ∧L (∀j : Z)(a[j ] = x).
11
Axioma 1: Asignación
I Axioma 1. wp(x := E,Q) ≡ def(E ) ∧L QxE .
I Ejemplo:
{??}
x := x + 1
{Q : x ≥ 7}
I Tenemos que ...
wp(x := x+1,Q) ≡ def(x + 1) ∧L Qxx+1
≡ True ∧L (x + 1) ≥ 7
≡ x ≥ 6
12
Axioma 1: Asignación
I Este axioma está justificado por la siguiente observación. Si
buscamos la precondición más débil para el siguiente
programa ...
{??}
x := E
{Q : x = 25}
I ... entonces tenemos wp(x := E,Q) ≡ def(E ) ∧L E = 25.
I Es decir, si luego de x := E queremos que x = 25, entonces
se debe cumplir E = 25 antes de la asignación!
13
Axioma 1: Asignación
I Otro ejemplo:
{??}
x := 2 * |x| + 1
{Q : x ≥ 5}
I Tenemos que ...
wp(x := 2 * |x| + 1,Q) ≡ def(2 ∗ |x |+ 1) ∧L Qx2∗|x |+1
≡ True ∧L 2 ∗ |x |+ 1 ≥ 5
≡ |x | ≥ 2
≡ x ≥ 2 ∨ x ≤ −2
14
Axioma 1: Asignación
I Un ejemplo más:
{??}
x := y*y
{Q : x ≥ 0}
I Tenemos que ...
wp(x := y*y,Q) ≡ def(y ∗ y) ∧L Qxy∗y
≡ True ∧L y ∗ y ≥ 0
≡ True
15
Demostraciones de corrección
I Dijimos que {P} S {Q} sii P ⇒L wp(S,Q).
I Es decir, queremos que P ⇒L wp(S,Q) capture el hecho de
que si S comienza en un estado que satisface P, entonces
termina y lo hace en un estado que satisface Q.
I Por ejemplo, la siguiente tripla de Hoare es válida ...
{P : x ≥ 10}
S: x := x+3
{Q : x 6= 4}
I ... puesto que:
I wp(S,Q) ≡ x 6= 1 y
I x ≥ 10⇒L x 6= 1.
16
Demostraciones de corrección
I La definición anterior implica que:
1. Si P ⇒L wp(S,Q), entonces {P} S {Q} es válida (i.e., es
verdadera).
2. Si P 6⇒L wp(S,Q), entonces {P} S {Q} no es válida (i.e., es
falsa).
I Por ejemplo: wp(x:=x+1, x ≥ 7) ≡ x ≥ 6.
I Como x ≥ 4 6⇒L x ≥ 6 (contraejemplo, x = 5), entonces se
concluye que
{P : x ≥ 4}
S: x := x+1
{Q : x ≥ 7}
no es válida.
17
Más axiomas
I Axioma 2. wp(skip,Q) ≡ Q.
I Axioma 3. wp(S1; S2,Q) ≡ wp(S1,wp(S2,Q)).
I Ejemplo:
{wp(y := 2*x,R)} ≡ {def(2∗ x) ∧L 2∗ x ≥ 6} ≡ {x ≥ 3}
y := 2*x;
{wp(x := y+1,Q)} ≡ {def(y + 1) ∧L y + 1 ≥ 7}
≡ {y ≥ 6}
x := y + 1
{Q : x ≥ 7}
18
Intercambiando los valores de dos variables
I Ejemplo: Recordemos el programa para intercambiar dos
variables numéricas.
I {wp(a := a + b,E2)}
≡ {def (a + b) ∧L (b = B0 ∧ (a + b)− b = A0)}
≡ {b = B0 ∧ a = A0} ≡ {E3}
a := a + b;
{wp(b := a - b,E1)}
≡ {def (a− b) ∧L (a− (a− b) = B0 ∧ a− b = A0)}
≡ {b = B0 ∧ a− b = A0} ≡ {E2}
b := a - b;
{wp(a := a - b,Q)}
≡ {def (a− b) ∧L (a− b = B0 ∧ b = A0)}
≡ {a− b = B0 ∧ b = A0} ≡ {E1}
a := a - b;
{Q} ≡ {a = B0 ∧ b = A0}
19
Intercambiando los valores de dos variables
I Como P ⇒ E3 ≡ wp(S ,Q), entonces podemos concluir que el
algoritmo es correcto respecto de su especificación.
I Observar que los estados intermedios que obtuvimos aplicando
wp son los mismos que hab́ıamos usado para razonar sobre la
corrección de este programa!
{a = A0 ∧ b = B0}
a := a + b;
{a = A0 + B0 ∧ b = B0}
b := a - b;
{a = A0 + B0 ∧ b = A0}
a := a - b;
{a = B0 ∧ b = A0}
I En lugar de razonar de manera informal, ahora podemos dar
una demostración de que estos estados describen el
comportamiento del algoritmo.
20
Recap: Axiomas wp
I Axioma 1. wp(x := E,Q) ≡ def(E ) ∧L QxE .
I Axioma 2. wp(skip,Q) ≡ Q.
I Axioma 3. wp(S1; S2,Q) ≡ wp(S1,wp(S2,Q)).
21
Alternativas
I Axioma 4. Si S = if B then S1 else S2 endif, entonces
wp(S,Q) ≡ def (B) ∧L
(
(B ∧ wp(S1,Q)) ∨
(¬B ∧ wp(S2,Q))
)
I Ejemplo:
{??}
S: if (x > 0) then y := x else y := -x endif
{Q : y ≥ 2}
I Tenemos que ...
wp(S,Q) ≡ (x > 0 ∧ x ≥ 2) ∨ (x ≤ 0 ∧ −x ≥ 2)
≡ (x ≥ 2) ∨ (x ≤ −2)
≡ |x | ≥ 2
22
Alternativas
I La definicion operacional que vimos para demostrar la
corrección de una alternativa es ahora un teorema derivado de
este axioma!
I Teorema. Si P ⇒ def (B) y
{P ∧ B} S1 {Q}
{P ∧ ¬B} S2 {Q}
entonces
{P} if B then S1 else S2 endif {Q}.
23
Alternativas
I Demostración.
[P ∧ B ⇒ wp(S1,Q)] ∧ [P ∧ ¬B ⇒ wp(S2,Q)]
≡ [¬(P ∧ B) ∨ wp(S1,Q)] ∧ [¬(P ∧ ¬B) ∨ wp(S2,Q)]
≡ [¬P ∨ ¬B ∨ wp(S1,Q)] ∧ [¬P ∨ B ∨ wp(S2,Q)]
≡ ¬P ∨
(
[¬B ∨ wp(S1,Q)] ∧[B ∨ wp(S2,Q)]
)
≡ P ⇒ [B ⇒ wp(S1,Q)] ∧ [¬B ⇒ wp(S2,Q)]
≡ P ⇒ [B ∧ wp(S1,Q)] ∨ [¬B ∧ wp(S2,Q)]
≡ P ⇒ def (B) ∧L
(
[B ∧ wp(S1,Q)] ∨ [¬B ∧ wp(S2,Q)]
)
≡ P ⇒ wp(if B then S1 else S2 endif,Q) �
24
Alternativas
I En el ejemplo anterior, vimos que:
{P : |x | ≥ 2}
S: if (x > 0) then y := x else y := -x endif
{Q : y ≥ 2}
I Veamos ahora la validez de esta tripla de Hoare por medio del
teorema anterior.
P ∧ B ⇒L wp(y := x,Q)
|x | ≥ 2 ∧ x > 0 ⇒L def (x) ∧L x ≥ 2 ≡ x ≥ 2 X
P ∧ ¬B ⇒L wp(y := -x,Q)
|x | ≥ 2 ∧ x ≤ 0 ⇒L def (x) ∧L −x ≥ 2 ≡ x ≤ −2 X
25
Asignación a elementos de una secuencia
I ¿Qué sucede con asignaciones de la forma b[i] := E?
I El Axioma 1 aplica a x := E, pero siendo x una variable! En
este caso, b es la variable en cuestión.
I Definición. Reescribimos b[i ] := E como b := setAt(b, i ,E ).
I En este caso, tenemos
def(setAt(b, i ,E )) = (def(E ) ∧ def(b) ∧ def(i))
∧L
(
0 ≤ i < |b|
)
.
I Observación: En el libro de D. Gries se usa la notación
(b; i ;E ) en lugar de setAt(b, i ,E ).
26
Asignación a elementos de una secuencia
I Aplicando el Axioma 1, tenemos:
wp(b[i ] := E ,Q)
≡ wp(b := setAt(b, i ,E ),Q)
≡ def (setAt(b, i ,E )) ∧L QbsetAt(b,i ,E)
≡
(
(def (b) ∧ def (i)) ∧L 0 ≤ i < |b|
)
∧ def(E )) ∧L QbsetAt(b,i ,E)
Dados 0 ≤ i , j < |b|, recordemos que:
setAt(b, i ,E )[j ] =
{
E si i = j
b[j ] si i 6= j
27
Asignación a elementos de una secuencia
I Ejemplo. Supongamos que i está definida y dentro del rango
de la secuencia b.
wp(b[i] := 5, b[i ] = 5)
≡ ((def(i) ∧L 0 ≤ i < |b|) ∧ def(5)) ∧L setAt(b, i , 5)[i ] = 5
≡ setAt(b, i , 5)[i ] = 5
≡ 5 = 5 ≡ True
28
Asignación a elementos de una secuencia
I Ejemplo. Con las mismas hipótesis.
wp(b[i] := 5, b[j ] = 2)
≡ setAt(b, i , 5)[j ] = 2
≡ (i 6= j ∧ setAt(b, i , 5)[j ] = 2) ∨ (i = j ∧ setAt(b, i , 5)[j ] = 2)
≡ (i 6= j ∧ b[j ] = 2) ∨ (i = j ∧ setAt(b, i , 5)[i ] = 2)
≡ (i 6= j ∧ b[j ] = 2) ∨ (i = j ∧ 5 = 2)
≡ i 6= j ∧ b[j ] = 2
29
Propiedades
I Monotońıa:
I Si Q ⇒ R entonces wp(S ,Q)⇒ wp(S ,R).
I Distributividad:
I wp(S ,Q) ∧ wp(S ,R)⇒ wp(S ,Q ∧ R),
I wp(S ,Q) ∨ wp(S ,R)⇒ wp(S ,Q ∨ R).
I “Excluded Miracle”:
I wp(S , false) ≡ false.
30
Corolario de la monotońıa
I Corolario: Si
I P ⇒ wp(S1,Q),
I Q ⇒ wp(S2,R),
entonces
I P ⇒ wp(S1;S2,R).
I Demostración.
P ⇒ wp(S1,Q) (por hipótesis)
⇒ wp(S1,wp(S2,R)) (monotońıa)
≡ wp(S1;S2,R) (Axioma 2)
31
Bibliograf́ıa
I David Gries - The Science of Programming
I Part II - The Semantics of a Small Language
I Chapter 7 - The Predicate Transformer wp
I Chapter 8 - The Commands skip, abort and Composition
I Chapter 9 - The Assignment Command
I Chapter 10 - The Alternative Command
32