PDF de programación - Tema 5 - Tecnología de la Programación

UNIVERSIDAD DE A CORUÑA
FACULTAD DE INFORMÁTICA

DEPARTAMENTO DE COMPUTACIÓN

Tecnología de la Programación

Ingeniería Técnica en Informática de Sistemas

Elena Mª Hernández Pereira

Óscar Fontenla Romero

Bloque didáctico II: Semántica de programas

Tema 5

o Título: El transformador de predicados wp

o Unidades de contenido

• Definición del transformador de predicados
• Propiedades del wp
• Estrategia de demostración de corrección

Tecnología de la programación - Elena Hernández & Oscar Fontenla

2

1

Tema 5: El wp

Definición y ejemplos

Bloque didáctico II:

Semántica de programas

o Definición: Predicado wp(S,R)

• Representa el conjunto de todos los estados tales

que, si la ejecución de S comienza en alguno de
ellos, está garantizado que termina en una cantidad
de tiempo finita y en un estado que satisfaga R

o Ejemplo:

• S: i:=i+1 y R: i £ 1
•
• Solución: wp(“i:=i+1”,i £ 1) = (i £ 0)

{(i, 0), (i, -1), (i, -2), …} ⇒ i £ 0

Tecnología de la programación - Elena Hernández & Oscar Fontenla

3

Tema 5: El wp

Definición y ejemplos

Bloque didáctico II:

Semántica de programas

o Ejemplos

• S: if x ‡ y then z:=x else z:=y R: z=max(x,y)
• wp(S,R)= T

• S: if x ‡ y then z:=x else z:=y R: z=y
• wp(S,R)= (y ‡ x)

• S: if x ‡ y then z:=x else z:=y R: z=y - 1
• wp(S,R)= F

o Dado un comando S, wp(S,T)

• Representa el conjunto de todos los estados tales que para

la ejecución de S que comienza en uno de ellos, se
garantiza su finalización

Tecnología de la programación - Elena Hernández & Oscar Fontenla

4

2

Tema 5: El wp

Definición y ejemplos

Bloque didáctico II:

Semántica de programas

o

{Q} S {R}
• Q, precondición y R, postcondición

o wp(S,R)

o

o

• Precondición más débil (weakest precondition)
{Q} S {R} alternativa a Q ⇒ wp(S,R)
{Q} S {R} es cierto EST(Q) ˝ wp(S,R)
• Es decir, exigimos que Q ⇒ wp(S,R) sea una tautología

o Decimos entonces que S satisface la corrección total

respecto a Q y R

Tecnología de la programación - Elena Hernández & Oscar Fontenla

5

Tema 5: El wp
Definición y ejemplos

Bloque didáctico II:

Semántica de programas

o La corrección parcial de S respecto a Q y R

se denota Q {S} R y equivale a:
• Si iniciamos S en un estado que satisface Q, y se

da que termina, entonces satisface R al acabar

• No garantiza la terminación de S

o Ej:

• T {while T do skip} T (tautología)

•

{T} while T do skip {T} (falsa)
 T ⇒wp(“while T do skip”,T)

Tecnología de la programación - Elena Hernández & Oscar Fontenla

6

3

Bloque didáctico II:

Semántica de programas

Tema 5: El wp

Propiedades

o Ley del milagro excluido

• wp(S,F) = F

o Distributividad de la conjunción
)

• wp(S, a ) wp(S, b ) = wp(S,ab

o Ley de monotonicidad

• Si a ⇒b entonces wp(S, a ) ⇒wp(S, b)

o Distributividad de la disyunción

• wp(S, a ) wp(S, b ) ⇒wp(S,ab
• wp(S, a ) wp(S, b ) wp(S,ab

)
) si S determinista

Tecnología de la programación - Elena Hernández & Oscar Fontenla

7

Tema 5: El wp

Casos extremos de especificación

Bloque didáctico II:

Semántica de programas

Tecnología de la programación - Elena Hernández & Oscar Fontenla

8

4

Tema 5: El wp

Demostración de corrección

Bloque didáctico II:

Semántica de programas

o Estrategia:
o Dado {Q} S {R} demostrar la corrección es lo

mismo que:
1. Calcular wp(S,R)
2. Demostrar que Q ⇒ wp(S,R)
o Fortalecer / Debilitar Q y R

Tecnología de la programación - Elena Hernández & Oscar Fontenla

9

Bloque didáctico II:

Semántica de programas

Tema 5: El wp

Ejercicios

o Determina wp(S,R) para:

Tecnología de la programación - Elena Hernández & Oscar Fontenla

10

5

Tema 5: El wp
Transiciones de estados

Bloque didáctico II:

Semántica de programas

o Trayectoria ⇒ secuencia de estados
o Traza ⇒ secuencia de instrucciones
o

La misma traza puede ser debida a distintas
trayectorias

o Trayectorias distintas para el mismo estado ⇒ trazas

distintas

o Programa determinista ⇒ aquel que para cualquier
estado inicial genera (como mucho) una única traza
• Mismo s0, varias trazas ⇒ no determinista
• Mismo s0 varias trayectorias ⇒ varias trazas ⇒ no

determinista

• Mismo s0, única trayectoria ⇒ determinista

Tecnología de la programación - Elena Hernández & Oscar Fontenla

11

Tema 5: El wp
Transiciones de estados

Bloque didáctico II:

Semántica de programas

o Programas equivalentes

• Para todo estado inicial tienen el mismo conjunto

de posibles estados finales y terminan o no, de
igual forma para cualquier estado inicial

o Ej:

•

•

i:=i+2 es equivalente a i:=i+1; i:=i+1
{x=2} S {y=10}



(a) y := x*5 (b) y := x+8

no son equivalentes

Tecnología de la programación - Elena Hernández & Oscar Fontenla

12

6