Slides TD Parcial1-61-70

Vista previa del material en texto

Axioma de Skip
Dada una postcondición Q y una operación skip (en C++, es un
bloque {} vacío), ¾cuál será su WP?
Si el programa no hace nada... ½El estado no cambia!
[skip] : wp({},Q) ≡ Q
Suele usarse cuando un if tiene alguna de sus ramas vacía.
Ejemplo
wp({}, {i = 0 ∧ j > 0}) ≡ {i = 0 ∧ j > 0}
29
Uso de Skip
Para calcular la wp de un programa como el siguiente:
if (i < 0) {i = 0;}
Primero reescribiremos el programa para que contenga las dos ramas
del if:
if (i < 0) {i = 0;} else {}
Y luego aplicaremos el axioma [If ] para todo el programa y [Skip]
para la segunda rama.
30
Ejercicios
Dada la siguiente especi�cación:
Intercambia dos posiciones si el contenido de la primera es mayor que
el de la segunda
void intercambiar(vector<int>& v, int i, int j)
Pre: v = v0 ∧ 0 ≤ i < j < |v |
Post: v [i ] = min(v0[i ], v0[j ]) ∧ v [j ] = max(v0[i ], v0[j ])
Veri�car si las siguiente implementación es correcta según la
especi�cación dada arriba.
1 if (v[i] > v[j]) {
2 tmp = v[j];
3 v[j] = v[i];
4 v[i] = tmp;
5 }
31
Técnicas de demostración
Recordemos: para probar la corrección de un programa S (sin ciclos)
con respecto a una precondición P y una postcondición Q,
necesitamos ejecutar dos pasos:
1. Calcular su WP, es decir, wp(S ,Q)
2. Probar que P =⇒ wp(S ,Q)
Ahora... ¾cómo probamos esa implicación?
I Una manera es asumir que P ≡ Verdadero, y mostrar que
entonces wp(S ,Q) también tiene que ser verdadero.
I Otra manera es partir del predicado P y transformarlo
planteando equivalencias o implicaciones hasta llegar a algo
que es sintácticamente igual a wp(S ,Q):
P ≡ P1 ≡ P2 =⇒ P3 · · · =⇒ wp(S ,Q)
3
Demostración de P =⇒ wp(S ,Q) (I)
Asumiendo que es verdadera
P ≡ 0 < i < |v | ∧ v [i ] > 1
Quiero ver que es verdadera
wp(S ,Q) ≡ 0 ≤ i ≤ |v | ∧ v [i ] > 0
.. entonces pruebo que P implica a cada una de las partes de la wp.
0 < i < |v | =⇒ 0 ≤ i ≤ |v | ?
0 < i =⇒ 0 ≤ i X
i < |v | =⇒ i ≤ |v | X
v [i ] > 1 =⇒ v [i ] > 0 X
Probé que asumiendo P ≡ Verdadero ambas partes de la WP son
verdaderas ⇒ la WP es Verdadera
4
Demostración de P =⇒ wp(S ,Q): otro método
Quiero probar que
P ≡ 0 < i < |v | ∧ v [i ] > 1 =⇒ wp(S ,Q) ≡ 0 ≤ i ≤ |v | ∧ v [i ] > 0
.. entonces aplico transformaciones a P hasta conseguir algo igual a la
WP, aprovechando que la implicación es transitiva: (si P =⇒ Q y si
Q =⇒ R, entonces P =⇒ R )
P
≡ 0 < i < |v | ∧ v [i ] > 1
[0 < i =⇒ 0 ≤ i ] =⇒ 0 ≤ i < |v | ∧ v [i ] > 1
[i < |v | =⇒ i ≤ |v |] =⇒ 0 ≤ i ≤ |v | ∧ v [i ] > 1
[i > 1 =⇒ i > 0] =⇒ 0 ≤ i ≤ |v | ∧ v [i ] > 0
wp(S ,Q)X
Con una cadena de implicaciones y equivalencias llegué de P a la
WP: entonces la implicación que quiero probar vale.
5
Corrección de programas con ciclos
int suma_y_duplica(vector<int> v, int k)
Pre: Verdadero
res = k;
i = 0;
Pc (precondición del ciclo)
while(i < v.size()){
res = res + v[i];
i = i + 1;
}
Qc (poscondición del ciclo)
res = res * 2;
Post: res = (k +
∑|v|−1
j=0 v [j ]) ∗ 2
S1
S2
S3
Para demostrar {Pre} S {Post} necesitamos probar que valen las triplas:
I {Pre} S1 {Pc},
I {Pc} S2 {Qc},
I {Qc} S3 {Post}
6
Corrección de programas con ciclos
Queremos demostrar que vale
{Pc} while(B) Sc ; {Qc}
Donde:
I B es la guarda (condición) del ciclo, y
I Sc es el cuerpo del ciclo.
Debemos demostrar:
I Corrección parcial
Si el ciclo termina, el estado �nal cumple Qc .
I Terminación
Luego de una cantidad �nita de iteraciones la condición B se
vuelve falsa y el ciclo termina.
7
Invariante de ciclo
Pc ≡ (i = 0 ∧ res = 0 ∧ n ≥ 0)
while(i <= n){
res = res + i;
i = i + 1;
}
Qc ≡ (res =
∑n
j=0 j)
Ejemplo con n = 6:
i res n
0 0 6
1 0 + 0 6
2 0 + 0 + 1 6
3 0 + 0 + 1 + 2 6
4 0 + 0 + 1 + 2 + 3 6
5 0 + 0 + 1 + 2 + 3 + 4 6
6 0 + 0 + 1 + 2 + 3 + 4 + 5 6
7 0 + 0 + 1 + 2 + 3 + 4 + 5 + 6 6
Invariante del ciclo:
(res =
i−1∑
j=0
j) ∧ 0 ≤ i ≤ n + 1
�res almacena la suma parcial
hasta i sin incluir, y i está en
rango�
8
Invariante de ciclo
I ≡ (res =
i−1∑
j=0
j) ∧ 0 ≤ i ≤ n + 1
I El invariante del ciclo expresa cuál es el trabajo computacional que
realiza el ciclo en cada iteración.
I Expresa el cómputo �parcial� realizado por el ciclo luego de cada
iteración incluso antes de �nalizar todas las iteraciones.
Un buen invariante de ciclo suele tener:
I El valor de las variables que se modi�can en cada iteración.
I Un caso particular importante es una variable en la que vamos
acumulando un resultado.
I El rango de valores entre los que se mueve la variable que itera.
9