Slides TD Parcial1-31-40

Vista previa del material en texto

Razonando sobre especificaciones
Sean dos contratos C1 y C2:
Problema C1
float C1(float a, float b)
Pre: a > 0
Post: res = π ∗ a2 ∗ b
Problema C2
float C2(float a, float b)
Pre: a > 0 ∧ b > 0
Post: res ≥ bπ ∗ a2 ∗ bc
Dado un programa P que es correcto con respecto a C1,
¿será correcto con respecto a C2?
13
Razonando sobre especificaciones
P es correcto respecto a C1...
Pre: a > 0
Programa P
Post: res = π ∗ a2 ∗ b
¿P será correcto respecto a C2?
Pre: a > 0 ∧ b > 0
Programa P
Post: res ≥ bπ ∗ a2 ∗ bc
I ¿Todos los inputs válidos de C2 son inputs válidos de C1?
I Sí 3
I ¿Todos los outputs válidos de C1 son outputs válidos de C2?
I Sí 3
14
Razonando sobre especificaciones
Dado un programa P que satisface una especificación C1, P será correcto
respecto a C2 si y sólo si:
I La preconidición de C2 es más fuerte que la precondición de C1, y
I La poscondición de C1 es más fuerte que la poscondición de C2.
Relación de fuerza: Decimos que la fórmula F es más fuerte que la
fórmula G si la siguiente expresión es una tautología:
F =⇒ G
Es decir, cualquier valuación que satisface F también debe satisfacer G .
15
Razonando sobre especificaciones
P es correcto respecto a C1...
Pre: a > 0
Programa P
Post: res = π ∗ a2 ∗ b
¿P será correcto respecto a C2?
Pre: a > 0 ∧ b > 0
Programa P
Post: res ≥ bπ ∗ a2 ∗ bc
I PreC2 es más fuerte que PreC1 :
Sí, porque a > 0 ∧ b > 0 =⇒ a > 0 para cualquier a y b 3
I PostC1 es más fuerte que PostC2 :
Sí, porque res = π ∗ a2 ∗ b =⇒ res ≥ bπ ∗ a2 ∗ bc para cualquier a y b 3
16
Corrección de un programa
Dado un contrato que especi�ca una Precondición y una Postcondición,
nos interesa probar formalmente que un programa S propuesto es
correcto con respecto a ese contrato.
Es decir, queremos probar que siempre que las entradas cumplan con la
Pre, la ejecución de nuestro programa llegará a un estado que cumple la
Post.
En esta clase veremos herramientas lógicas para poder demostrar esa
propiedad.
3
Estado de un programa
Llamamos estado de un programa al conjunto de valores de cada una
de sus variables.
Para razonar sobre estados escribimos predicados que caracterizan una o
más propiedades que cumple un estado del programa:
E : {i = a ∧ j = b}
E representa al conjunto de estados donde vale que i = a y j = b
Al ejecutar una instrucción, el estado del programa cambia, y
podemos describir esos cambios con predicados:
E0 : {i = a ∧ j = b}
i = i + j;
E1 : {i = a + b ∧ j = b}
j = i - j;
E2 : {i = a + b ∧ j = a}
i = i - j;
E3 : {i = b ∧ j = a}
4
Triplas de Hoare
Una Tripla de Hoare consta de una Precondición P, una
Postcondición Q y de un programa S , y se escribe:
{P} S {Q}
y será Verdadera si, para todo estado del programa que satisface P,
la ejecución de S siempre lo deja en un estado que satisface Q.
Por ejemplo, la tripla de Hoare de la slide anterior
{i = a ∧ j = b} i= i+j; j = i-j; i = i-j; {i = b ∧ j = a}
es una tripla de Hoare verdadera... al menos intuitivamente.
5
Triplas de Hoare y corrección
Un programa S con una precondición Pre y una postcondición Post
será correcto con respecto a éstas si la tripla de Hoare
{Pre} S {Post}
es verdadera. Pero... ¾cómo hacemos esta prueba?
Una metodología es establecer un camino entre la Pre y la Post en base
a la secuencia de instrucciones S1 . . . Sn del programa:
{E0} S1 {E1} S2 {E2} . . . {En−1} Sn {En}
de manera que Pre =⇒ E0,En =⇒ Post, y cada una de las triplas
{Ei} Si+1{Ei+1}
sea verdadera.½Ahora sólo necesitamos un mecanismo para calcular los Ei
intermedios!
6
Transformadores de Predicados
Una semántica de transformadores de predicados es una manera
de especi�car el comportamiento de cada instrucción de un
programa imperativo.
Consiste en de�nir, para cada instrucción, un transformador de
predicados que codi�ca el efecto de ejecutar la operación en un
predicado que describe el estado antes (o después) de ejecutar la
instrucción.
En la literatura existen principalmente dos transformadores propuestos
por Dijkstra:
I La postcondición más fuerte (sp)
I La precondición más débil (wp)
7
Transformadores de Predicados: Strongest Postcondition
(sp)
La Postcondición más fuerte (sp) es el transformador que, dada una
operación S y una precondición P, calcula un predicado Q tal que
{P} S {Q}
y, para cualquier Q ′ que cumpla {P} S {Q ′}, vale Q =⇒ Q ′.
Intuitivamente: la sp calcula lo máximo que se puede asumir luego
de ejecutar el código a partir de una condicion inicial dada.
Calcula �hacia adelante�.
8