Slides TD Parcial1-71-80

Vista previa del material en texto

Corrección parcial
Para demostrar corrección parcial de
{Pc} while(B) Sc ; {Qc}
necesitamos proponer un invariante del ciclo I y demostrar que:
I Pc =⇒ I
El invariante vale antes de entrar al ciclo
I {I ∧ B = true} Sc {I}
El cuerpo del ciclo preserva la validez del invariante
I (I ∧ B = false) =⇒ Qc
Al salir del ciclo vale la poscondición Qc .
10
Corrección parcial - Ejemplo
Pc ≡ (i = 0 ∧ res = 0 ∧ n ≥ 0)
while(i <= n){
res = res + i;
i = i + 1;
}
Qc ≡ (res =
∑n
j=0 j)
Proponemos el siguiente invariante:
I ≡ (res =
i−1∑
j=0
j) ∧ 0 ≤ i ≤ n + 1
11
Corrección parcial - Ejemplo
Veamos que Pc =⇒ I
Asumimos Pc : (i = 0 ∧ res = 0 ∧ n ≥ 0)
Reemplazamos i y res en I
0 =
0∑
j=0
j ∧ 0 ≤ 0 ≤ n + 1
≡ 0 =
0∑
j=0
j ∧ 0 ≤ 0 ∧ 0 ≤ n + 1
≡ 0 = 0 ∧ 0 ≤ 0 ∧ 0 ≤ n + 1
≡ 0 ≤ n + 1
[hip. Pc ] ≡ Verdadero
12
Corrección parcial - Ejemplo
Veamos que (I ∧ B = true) =⇒ wp(Sc , I)
wp(Sc , I)
≡ wp(res = res + i; i = i + 1, res =
i−1∑
j=0
j ∧ 0 ≤ i ≤ n + 1)
[Seq] ≡ wp(res = res + i,wp(i = i + 1, res =
i−1∑
j=0
j ∧ 0 ≤ i ≤ n + 1))
[Asig ] ≡ wp(res = res + i, def (i + 1) ∧ res =
i+1−1∑
j=0
j ∧ 0 ≤ i + 1 ≤ n + 1)
[def ,Asig ] ≡ def (res + i) ∧ res + i =
i∑
j=0
j ∧ 0 ≤ i + 1 ≤ n + 1
[def ] ≡ res + i =
i∑
j=0
j ∧ 0 ≤ i + 1 ≤ n + 1
13
Corrección parcial - Ejemplo
Veamos que (I ∧ B = true) =⇒ wp(Sc , I)
Asumimos (I ∧ B = true)
≡ res =
i−1∑
j=0
j ∧ 0 ≤ i ≤ n + 1 ∧ i ≤ n
≡ res =
i−1∑
j=0
j ∧ 0 ≤ i ≤ n
Recordemos wp(Sc , I)
≡ res + i =
i∑
j=0
j ∧ 0 ≤ i + 1 ≤ n + 1
[Rp. res, simp. i ] ≡
(
(
i−1∑
j=0
j) + i =
i∑
j=0
j
)
∧ −1 ≤ i ≤ n
[Reordeno sum., hip.] ≡ Verdadero ∧ Verdadero
14
Corrección parcial - Ejemplo
Veamos que (I ∧ B = false) =⇒ Qc
Asumimos (I ∧ B = false)
≡ res =
i−1∑
j=0
j ∧ 0 ≤ i ≤ n + 1 ∧ i > n
[simp. i ] ≡ res =
i−1∑
j=0
j ∧ i = n + 1
=⇒ res =
n+1−1∑
j=0
j
≡ res =
n∑
j=0
j
≡ Qc
15
Función variante
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 n n + 1 - i
0 6 7
1 6 6
2 6 5
3 6 4
4 6 3
5 6 2
6 6 1
7 6 0
Función variante:
fv = n + 1− i
16
Terminación
Para demostrar terminación de
{Pc} while(B) Sc ; {Qc}
necesitamos proponer una función variante fv y demostrar que:
I {I ∧ B = true ∧ fv = fv0} Sc {fv < fv0}
La función variante es estrictamente decreciente al ejecutar una
iteración del ciclo.
I I ∧ fv ≤ 0 =⇒ B = false
Si la función variante llega a cero, entonces la condición del
ciclo se vuelve falsa.
17
Terminación - Ejemplo
Si nuestra función variante es
fv = n + 1− i
tenemos que mostrar que
I {I ∧ B = true ∧ n − i − 1 = fv0} Sc {n + 1− i < fv0}
I I ∧ n + 1− i ≤ 0 =⇒ B = false
18
Terminación - Ejemplo
Veamos que
I ∧ B = true ∧ n + 1− i = fv0 =⇒ wp(Sc , n + 1− i < fv0)
wp(Sc , n + 1− i < fv0)
≡ wp(res = res + i; i = i + 1, n + 1− i < fv0)
[Seq] ≡ wp(res = res + i,wp(i = i + 1, n + 1− i < fv0))
[Asig , def ] ≡ wp(res = res + i, n + 1− (i + 1) < fv0)
[Asig ] ≡ n + 1− i − 1 < fv0
[Asig ] ≡ n − i < fv0
I ∧ B = true ∧ n + 1− i = fv0
=⇒ n + 1− i = fv0
Reemplazo fv0 en wp(Sc , n + 1− i < fv0)
n − i < fv0
≡ n − i < n + 1− i
≡ Verdadero
19