Slides TD Parcial1-41-50

Vista previa del material en texto

Strongest Postcondition (sp): Ejemplo
Sea la siguiente tripla de Hoare:
{a > 0 ∨ b > 0} c = a*a + b*b {c > 0}
¾Es verdadera?½Sí!
¾es {c > 0} la SP del programa
c = a*a + b*b
con precondición {a > 0 ∨ b > 0)}? ½No!
La postcondición más fuerte es {c = a2 + b2}
½Notar que {c = a2 + b2} =⇒ {c > 0}!
Estrategia de demostración de corrección usando SP:
Calculo SP en base a programa + Pre y luego veri�co
SP =⇒ Post.
9
Transformadores de Predicados: Weakest Precondition (wp)
La Precondición más débil (wp) es el transformador que, dada una
operación S y una postcondición Q, calcula un predicado P tal que
{P} S {Q}
y, para cualquier P ′ que cumpla {P ′} S {Q}, vale P ′ =⇒ P.
Intuitivamente: la wp calcula la mínima condición inicial necesaria
para poder satisfacer, luego de ejecutar nuestro código, la condición
�nal buscada.
Calcula �hacia atrás�.
En TD3 usaremos la WP como transformador de predicados.
10
Weakest Precondition (wp): Ejemplo
Sea la tripla de Hoare del ejemplo anterior:
{a > 0 ∨ b > 0} c = a*a + b*b {c > 0}
¾es {a > 0 ∨ b > 0} la WP del programa
c = a*a + b*b
con postcondición {c > 0}? ½No!
La precondición más débil es {a 6= 0 ∨ b 6= 0}.
½Notar que {a > 0 ∨ b > 0} =⇒ {a 6= 0 ∨ b 6= 0}!
Estrategia de demostración de corrección usando WP:
Calculo WP en base a programa + Post y luego veri�co
Pre =⇒ WP.
11
Weakest Precondition
Notaremos wp(S ,Q) la precondición más débil de un programa
S = S1 . . . Sn con respecto a una postcondición Q.
Volviendo a nuestra estrategia de demostración
{E0} S1 {E1} S2 {E2} . . . {En−1} Sn {En}
Fijaremos En = Post (porque la WP calcula hacia atrás)
y Ei = wp(Si+1,Ei+1) para i = 0 . . . n − 1
(es decir cada wp está en función de la siguiente en la cadena)
Falta mostrar que Pre =⇒ wp(S1,E1)
Daremos reglas para calcular la WP para cada Si de un programa, y las
aplicaremos hasta conseguir un predicado �nal P
12
Lenguaje: C++ simpli�cado
C++ es complejo de describir:
I Especi�cación en castellano: pdf de 2000 páginas
I Especi�cación formal: paper de 120 hojas + 12000 líneas de
código de demostrador automático.
Intentar demostrar un programa C++ genérico sería excesivamente
complejo para el alcance de nuestra materia varias materias.
13
https://isocpp.org/std/the-standard
https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.636.7164&rep=rep1&type=pdf
Lenguaje: C++ simpli�cado
De�niremos un subconjunto reducido de C++ que usaremos para
describir los algoritmos en esta parte de la materia.
I Tipos: int, bool, char, float, vector<T>.
El programa se asume correctamente tipado.
I Operaciones de vector<T>:
I v.size(), v[i], ==, !=.
I Inicializar con tamaño N: v = vector<T>(N)
I No se permite modi�car el tamaño.
I Las variables se asumen todas de�nidas
I Condicionales: Sólo if-then-else; sin switch ni operador
ternario (?:)
I Ciclos: Sólo while ; sin break ni continue
I No hay return expr, en su lugar vamos a asignar valores a una
variable especial res y su valor en el estado �nal será el valor de
retorno.
14
Axioma de Asignación (I)
Dada una postcondición Q y una asignación de la forma x = Expr;,
con Expr alguna expresión, ¾cuál será su WP?
La instrucción x = Expr está pisando la variable x con el valor de la
expresión Expr.
Ejemplo: Si quiero que esta tripla sea verdadera...¾quién debe ser P?
{Px + 4 > 0} x = x + 4 {x > 0}
Eso signi�ca que cualquier condición que querramos que cumpla x en
Q (es decir, luego de ejecutar la instrucción)... ½debe ser cumplida
también por Expr!
¾Cómo se traduce esto a la WP?
15
Axioma de Asignación (II)
Si Q tenía condiciones sobre x ... necesitamos chequear esas mismas
condiciones sobre Expr . ½También necesitamos asegurar que Expr no
se inde�ne!
I Lo primero se consigue reemplazando sintácticamente cada
aparición libre de x en Q por Expr . Esto se nota Q[x ← Expr ].
I Lo segundo se consigue con un predicado auxiliar def (Slide: 20)
que nos da las condiciones para que una expresión no se
inde�na.
[Asig ] : wp(x = Expr,Q) ≡ def (Expr) ∧ Q[x← Expr]
16
WP de Asignación: Ejemplos
wp(i = j + 3, {i ≥ 5})
[Asig ] ≡def (j+3) ∧ {i ≥ 5}[i ← j + 3]
[def , i : j + 3] ≡Verdadero ∧ j + 3 ≥ 5
≡j ≥ 2
wp(i = 1, {i ≥ 0})
[Asig ] ≡def (1) ∧ {i ≥ 0}[i ← 1]
[def , i : 1] ≡Verdadero ∧ 1 ≥ 0
≡Verdadero
17
Axioma de Asignación � vectores
¾Qué pasa cuando asigno a una posición de un vector?
vec[i] = Expr
Esto no sigue la forma del Axioma de Asignación. Necesitamos algo
de la forma:
vec = [una copia de vec, pero con Expr en la posición i]
¾Y cómo notamos eso?
(vec; i: Expr)
wp(vec[i] = Expr,Q) ≡ wp(vec = (vec; i: Expr),Q)
≡ def ((vec; i: Expr)) ∧ Q[vec ← (vec; i: Expr)]
18