Slides TD Parcial1-81-92

Vista previa del material en texto

Terminación - Ejemplo
Veamos que I ∧ fv ≤ 0 =⇒ B = false
Asumimos I ∧ fv ≤ 0
≡ res =
i−1∑
j=0
j ∧ 0 ≤ i ≤ n + 1 ∧ n + 1− i ≤ 0
=⇒ i ≤ n + 1 ∧ n + 1 ≤ i
=⇒ i = n + 1
=⇒ i > n
≡ B = false
20
Ejemplo con vector
Dado el siguiente ciclo y su pre y pos condición, queremos ver que vale
{Pc} S {Qc}.
Pc ≡ (i = 0 ∧ v = v0)
while(i < v.size()){
v[i] = v[i] + 1;
i = i + 1;
}
Qc ≡ |v | = |v0| ∧ (∀j : int)(0 ≤ j < |v | =⇒ v [j ] = v0[j ] + 1)
Proponemos el siguiente invariante:
I ≡|v | = |v0|
∧ (∀j : int)(0 ≤ j < i =⇒ v [j ] = v0[j ] + 1)
∧ (∀j : int)(i ≤ j < |v | =⇒ v [j ] = v0[j ])
∧ 0 ≤ i ≤ |v |
21
Ejemplo con vector
Veamos que Pc =⇒ I
Asumimos Pc : (i = 0 ∧ v = v0)
Reemplazamos i y v en I:
|v0| = |v0|
∧ (∀j : int)(0 ≤ j < 0 =⇒ v0[j ] = v0[j ] + 1)
∧ (∀j : int)(0 ≤ j < |v0| =⇒ v0[j ] = v0[j ])
∧ 0 ≤ 0 ≤ |v0|
≡ Verdadero
∧ Verdadero
∧ Verdadero
∧ Verdadero
22
Ejemplo con vector
Veamos que (I ∧ B = true) =⇒ wp(Sc , I)
wp(Sc , I)
≡ wp(v[i] = v[i] + 1; i = i + 1;, I)
[Seq] ≡ wp(v[i] = v[i] + 1,wp(i = i + 1, I))
[Asig ] ≡ wp(v[i] = v[i] + 1, def (i + 1) ∧ I[i ← i + 1])
[Asigvec, def ] ≡ wp(v = (v; i: v[i] + 1), I[i ← i + 1])
[Asig ] ≡ def ((v ; i : v [i ] + 1)) ∧ I[i ← i + 1][v ← (v ; i : v [i ] + 1)]
[def ] ≡ 0 ≤ i < |v | ∧ I[i ← i + 1][v ← (v ; i : v [i ] + 1)]
[Rp. i ] ≡ 0 ≤ i < |v | ∧ (|v | = |v0|
∧ (∀j : int)(0 ≤ j < i + 1 =⇒ v [j ] = v0[j ] + 1)
∧ (∀j : int)(i + 1 ≤ j < |v | =⇒ v [j ] = v0[j ])
∧ 0 ≤ i + 1 ≤ |v |)[v ← (v ; i : v [i ] + 1)]
23
Ejemplo con vector
(continua)
[Rp. v ] ≡ 0 ≤ i < |v | ∧ (|(v ; i : v [i ] + 1)| = |v0|
∧ (∀j : int)(0 ≤ j < i + 1 =⇒ (v ; i : v [i ] + 1)[j ] = v0[j ] + 1)
∧ (∀j : int)(i + 1 ≤ j < |(v ; i : v [i ] + 1)| =⇒ (v ; i : v [i ] + 1)[j ] = v0[j ])
∧ 0 ≤ i + 1 ≤ |(v ; i : v [i ] + 1)|)
[Asigvec] ≡ 0 ≤ i < |v | ∧ (|v | = |v0|
∧ (∀j : int)(0 ≤ j < i + 1 =⇒ (v ; i : v [i ] + 1)[j ] = v0[j ] + 1)
∧ (∀j : int)(i + 1 ≤ j < |v | =⇒ (v ; i : v [i ] + 1)[j ] = v0[j ])
∧ 0 ≤ i + 1 ≤ |v |)
[Rango i ] ≡ 0 ≤ i < |v | ∧ (|v | = |v0|
∧ (∀j : int)(0 ≤ j < i + 1 =⇒ (v ; i : v [i ] + 1)[j ] = v0[j ] + 1)
∧ (∀j : int)(i + 1 ≤ j < |v | =⇒ (v ; i : v [i ] + 1)[j ] = v0[j ])
24
Ejemplo con vector
(continua)
[Asigvec] ≡ 0 ≤ i < |v | ∧ (|v | = |v0|
∧ (∀j : int)(0 ≤ j < i + 1 =⇒ (v ; i : v [i ] + 1)[j ] = v0[j ] + 1)
∧ (∀j : int)(i + 1 ≤ j < |v | =⇒ v [j ] = v0[j ])
[Sep. j = i ] ≡ 0 ≤ i < |v | ∧ (|v | = |v0|
∧ (∀j : int)(0 ≤ j < i =⇒ (v ; i : v [i ] + 1)[j ] = v0[j ] + 1)
∧ (v ; i : v [i ] + 1)[i ] = v0[i ] + 1
∧ (∀j : int)(i + 1 ≤ j < |v | =⇒ v [j ] = v0[j ])
[Asigvec] ≡ 0 ≤ i < |v | ∧ (|v | = |v0|
∧ (∀j : int)(0 ≤ j < i =⇒ v [j ] = v0[j ] + 1)
∧ v [i ] + 1 = v0[i ] + 1
∧ (∀j : int)(i + 1 ≤ j < |v | =⇒ v [j ] = v0[j ])
[Simp.] ≡ 0 ≤ i < |v | ∧ (|v | = |v0|
∧ (∀j : int)(0 ≤ j < i =⇒ v [j ] = v0[j ] + 1)
∧ v [i ] = v0[i ] ∧ (∀j : int)(i + 1 ≤ j < |v | =⇒ v [j ] = v0[j ])
25
Ejemplo con vector
(continua)
[caso i = j ] ≡ 0 ≤ i < |v | ∧ (|v | = |v0|
∧ (∀j : int)(0 ≤ j < i =⇒ v [j ] = v0[j ] + 1)
∧ (∀j : int)(i ≤ j < |v | =⇒ v [j ] = v0[j ])
≡ wp(Sc , I)← ½recordemos qué estabamos calculando!
Con esto debemos probar que
(I ∧ B = true) =⇒ wp(Sc , I)
26
Ejemplo con vector
Veamos que (I ∧ B = true) =⇒ wp(Sc , I)
Asumimos (I ∧ B = true)
≡ |v | = |v0|
∧ (∀j : int)(0 ≤ j < i =⇒ v [j ] = v0[j ] + 1)
∧ (∀j : int)(i ≤ j < |v | =⇒ v [j ] = v0[j ])
∧ 0 ≤ i<|v |
Esto es exactamente igual que wp(Sc , I), por lo tanto lo implica.
27
Ejemplo con vector
Veamos que (I ∧ B = false) =⇒ Qc
Asumimos (I ∧ B = false)
≡ |v | = |v0|
∧ (∀j : int)(0 ≤ j < i =⇒ v [j ] = v0[j ] + 1)
∧ (∀j : int)(i ≤ j < |v | =⇒ v [j ] = v0[j ])
∧ 0 ≤ i ≤ |v | ∧ i ≥ |v |
≡ |v | = |v0|
∧ (∀j : int)(0 ≤ j < i =⇒ v [j ] = v0[j ] + 1)
∧ (∀j : int)(i ≤ j < |v | =⇒ v [j ] = v0[j ])
∧ i = |v |
[Rp. i ] =⇒ |v | = |v0|
∧ (∀j : int)(0 ≤ j < |v | =⇒ v [j ] = v0[j ] + 1)
∧ (∀j : int)(|v | ≤ j < |v | =⇒ v [j ] = v0[j ])
[Rango ∀ vacio] ≡ |v | = |v0| ∧ (∀j : int)(0 ≤ j < |v | =⇒ v [j ] = v0[j ] + 1)
≡ Qc
28
Ejemplo con vector
¾Qué función variante podemos utilizar?
while(i < v.size()){
v[i] = v[i] + 1;
i = i + 1;
}
Proponemos la siguiente función variante:
fv = |v | − i
Tenemos que mostrar que:
I {I ∧ B = true ∧ |v | − i = fv0} Sc {|v | − i < fv0}
I I ∧ |v | − i ≤ 0 =⇒ B = false
29
Ejemplo con vector
Veamos que I ∧ B = true ∧ |v | − i = fv0 =⇒ wp(Sc , |v | − i < fv0)
wp(Sc , |v | − i < fv0)
≡ wp(v[i] = v[i] + 1; i = i + 1;, |v | − i < fv0)
[Seq] ≡ wp(v[i] = v[i] + 1,wp(i = i + 1, |v | − i < fv0))
[Asig , def ] ≡ wp(v[i] = v[i] + 1, |v | − (i + 1) < fv0)
[Asigvec, simp.] ≡ wp(v = (v; i: v[i] + 1), |v | − i − 1 < fv0)
[Asig ] ≡ def (v ; i : v [i ] + 1) ∧ |(v ; i : v [i ] + 1)| − i − 1 < fv0
[def ,Asigvec] ≡ 0 ≤ i < |v | ∧ |v | − i − 1 < fv0
I ∧ B = true ∧ |v | − i = fv0
=⇒ 0 ≤ i ≤ |v | ∧ i < |v | ∧ |v | − i = fv0
=⇒ 0 ≤ i < |v | ∧ |v | − i = fv0
=⇒ 0 ≤ i < |v | ∧ |v | − i − 1 < fv0
ya que |v | − i − 1 < |v | − i
30
Ejemplo con vector
Veamos que I ∧ fv ≤ 0 =⇒ B = false
Asumimos I ∧ fv ≤ 0
=⇒ 0 ≤ i ≤ |v | ∧ |v | − i ≤ 0
=⇒ 0 ≤ i ≤ |v | ∧ |v | ≤ i
=⇒ i = |v |
=⇒ i ≥ |v |
≡ B = false
31