Slides TD Parcial1-51-60

Vista previa del material en texto

Apartado: la expresión (vec; i: Expr)
(vec; i: Expr) es una expresión de tipo vector<T> que representa al
vector resultante de asignar en el vector vec de tipo vector<T> la
expresión Expr (de tipo T) a la posición indicada por la expresión i. Se
inde�ne si Expr es inde�nida o i < 0 o i ≥ |vec |.
Para poder manipularla en una demostración necesitamos reglas que nos
permitan transformarla:
La posición i tiene el contenido nuevo:
[asigvec1] (vec; i: Expr)[i ] ≡ Expr
Las posiciones (válidas) distintas a i tienen el contenido original:
[asigvec2] 0 ≤ j < |vec | ∧ j 6= i =⇒ (vec; i: Expr)[j ] ≡ vec[j]
Asignar a una posición no cambia la longitud:
[asigvec3] |(vec; i: Expr)| ≡ |vec|
19
Apartado: el predicado def
El predicado def indica que una expresión Expr está bien de�nida.
Asume que no hay errores de tipo en la expresión.
I def (x) ≡ Verdadero para toda variable x ;
I def (expresión aritmética) ≡ condiciones matemáticas para que
la expresión no se inde�na;
I def (expresión booleana) ≡ condiciones de la lógica de
cortocircuito para que la expresión no se inde�na;
I def (vec[i]) ≡ 0 ≤ i ≤ |vec | para vec de tipo vector<T>;
I def ((vec; i: Expr)) ≡ 0 ≤ i ≤ |vec | ∧ def (Expr) para vec de
tipo vector<T>.
def (i + 1) ≡ Verdadero
def ((x*y) / z) ≡ z 6= 0
def (0 <= i < |v| && v[i]>0) ≡ 0 ≤ i < |v |
def (v[i] + v[2*i]) ≡ 0 ≤ i < |v |/2
def ((v1; i+1: v2[i-1])) ≡ 0 ≤ i + 1 < |v1| ∧ 0 ≤ i − 1 < |v2|
20
WP de asignación en vectores: Ejemplos
wp(v[i] = v[i]+1, {v [i ] ≥ 5})
[asigvec] ≡wp(v = (v; i: v[i]+1), {v [i ] ≥ 5})
[Asig ] ≡0 ≤ i < |v | ∧ def (v [i ] + 1) ∧ {v [i ] ≥ 5}[v ← (v; i: v[i]+1)
[def ,Rp.v ] ≡0 ≤ i < |v | ∧ {(v; i: v[i]+1)[i ] ≥ 5}
[asigvec1] ≡0 ≤ i < |v | ∧ {v [i ] + 1 ≥ 5}
[simplifico] ≡0 ≤ i < |v | ∧ {v [i ] ≥ 4}
21
WP de asignación en vectores: Ejemplos
wp(v[i] = v[i-1]+1, {i + 1 < |v | ∧ v [i + 1] ≥ v [i ]})
[asigvec] ≡wp(v = (v; i: v[i-1]+1), {i + 1 < |v | ∧ v [i + 1] ≥ v [i ]}
[Asig ] ≡def ((v; i: v[i-1]+1))∧
{i + 1 < |v | ∧ v [i + 1] ≥ v [i ]}[v ← (v; i: v[i-1]+1)]
[def ,Rp.v ] ≡0 ≤ i < |v | ∧ def (v [i − 1] + 1) ∧ i + 1 < |(v; i: v[i-1]+1)|
∧ (v; i: v[i-1]+1)[i + 1] ≥ (v; i: v[i-1]+1)[i ]
[asigvec123] ≡0 ≤ i < |v | ∧ 0 ≤ i − 1 < |v | ∧ i + 1 < |v |
∧ v [i + 1] ≥ v [i − 1] + 1
≡0 < i < |v | − 1 ∧ v [i + 1] ≥ v [i − 1] + 1
22
WP de asignación en vectores: Ejemplos
wp(v[i] = v[i]+1, {(∀j : int) 0 ≤ j < |v | =⇒ v [j ] > 0})
[asigvec] ≡wp(v = (v; i: v[i]+1), {(∀j : int) 0 ≤ j < |v | =⇒ v [j ] > 0})
[Asig ] ≡def ((v; i: v[i]+1)) ∧
{(∀j : int) 0 ≤ j < |v | =⇒ v [j ] > 0}[v ← (v; i: v[i]+1)]
[Rp.v ] ≡0 ≤ i < |v |∧
(∀j : int) 0 ≤ j < |(v; i: v[i]+1)| =⇒ (v; i: v[i]+1)[j ] > 0
[asigvec3] ≡0 ≤ i < |v | ∧ (∀j : int) 0 ≤ j < |v | =⇒ (v; i: v[i]+1)[j ] > 0
[saco i = j ] ≡0 ≤ i < |v | ∧ (∀j : int) (0 ≤ j < |v | ∧ j 6= i =⇒ v [j ] > 0)
∧ (v; i: v[i]+1)[i ] > 0
≡0 ≤ i < |v | ∧ (∀j : int) 0 ≤ j < |v | ∧ j 6= i =⇒ v [j ] > 0
∧v [i ] > −1
23
Axioma de Composición Secuencial
Dada una postcondición Q y una secuencia de instrucciones S1; S2,
¾cuál será su WP? Veamos qué hace el programa:
I Partirá de un estado que cumpla P1 ≡ wp(S1;S2,Q) (lo que
queremos averiguar);
I ejecutará S1, llegando a un estado donde vale algún Q1;
I y �nalmente ejecutará S2, llegando a un estado donde vale Q.
Es decir, deberán cumplirse las siguientes triplas de Hoare:
{P1} S1 {Q1} y {Q1} S2 {Q}
..pero ¾quién debe ser Q1?... ½es wp(S2,Q)!
[Seq] : wp(S1;S2,Q) ≡ wp(S1,wp(S2,Q))
24
WP de Secuencia: Ejemplo 1 � swap
wp(i=i+j; j=i-j; i=i-j;, {i = b ∧ j = a})
[Seq x 2] ≡wp(i=i+j,wp(j=i-j,wp(i=i-j, {i = b ∧ j = a})))
[Asig x 3] ≡{i = b ∧ j = a}[i ← i − j ][j ← i − j ][i ← i + j ]
[i : i − j ] ≡{i − j = b ∧ j = a}[j ← i − j ][i ← i + j ]
[j : i − j ] ≡{i − (i − j) = b ∧ i − j = a}[i ← i + j ]
[i : j + i ] ≡{(i + j)− ((i + j)− j) = b ∧ (i + j)− j = a}
[simplif .] ≡{j = b ∧ i = a}
25
WP de Secuencia: Ejemplo 2
wp(i = i + 1; j = 2*j, {j > 2 ∗ i})
[Seq] ≡wp(i = i + 1,wp(j = 2*j, {j > 2 ∗ i}))
[Asig ] ≡def (i + 1)∧wp(j = 2*j, {j > 2 ∗ i})[i ← i + 1]
[Asig , def (i + 1)] ≡(def (2 ∗ j)∧{j > 2 ∗ i}[j ← 2 ∗ j ])[i ← i + 1]
[j : 2 ∗ j , def (2 ∗ j)] ≡{2 ∗ j > 2 ∗ i}[i ← i + 1]
[i : i + 1] ≡2 ∗ j > 2 ∗ (i + 1)
≡j > i + 1
26
Axioma de if-then-else
Dada una postcondición Q y un código de la forma if (cond) S1
else S2 ¾Cual será su WP?
La postcondición Q re�eja cómo quedó el estado del programa
después de ejecutar el if. Tenemos dos rutas posibles de ejecución:
I cond fue true → se ejecutó la rama S1;
I cond fue false → se ejecutó la rama S2.
¾Cuáles son las precondiciones mínimas para que, luego de ejecutar
S1 o S2, cumplir con Q? wp(S1,Q) y wp(S2,Q)
Si se cumplía cond, se debía cumplir wp(S1,Q), y si no, se debía
cumplir wp(S2,Q). En lógica:
[If ] : wp(if (cond) S1 else S2) ≡ def (cond)∧
(cond = true ∧ wp(S1,Q)) ∨ (cond = false ∧ wp(S2,Q))
27
WP de if-then-else: ejemplo
wp(if (i < 0) j = -i; else j = i;, j ≥ i)
[If ] ≡def (i < 0) ∧ {(i < 0 ∧ wp(j = -i,Q) ∨ (i ≥ 0 ∧ wp(j = i,Q))}
[Asig ] ≡{(i < 0 ∧ −i ≥ i) ∨ (i ≥ 0 ∧ i ≥ i)}
≡{(i < 0 ∧ 0 ≥ 2 ∗ i) ∨ i ≥ 0}
≡{(i < 0 ∧ 0 ≥ i) ∨ i ≥ 0}
≡{(i < 0 ∨ i ≥ 0}
≡Verdadero
28