• Author / Uploaded
• Sara Perez

Citation preview

Universidad Mayor de San Andrés Facultad de ciencias puras y naturales Carrera de Informática Semestre II – 2019

INF-282 “Transformador de predicados” Aux. Rolando Troche Venegas Aux. Daysi M. Quispe Guarachi

Practica nro. 2

Nota:   

Reutilizar hojas de papel (obligatorio) Se debe entregar las practicas a un solo auxiliar. Se coordinará la entrega de prácticas con su respectivo auxiliar.

Transformador de predicados 1.

Calcular la precondición más débil: wp(x := y;skip;z := y;k := x + 1,k > w)

2.

Calcular la precondición más débil, wp(S, R) Donde:

3.

Calcular la precondición más débil, wp(S1;DO;S2;IF;S3,R) Donde: :

skip;x := n;y := 1

: :

do x > 0 → y := y ∗ x;x := x − 1 od z := y

IF S3

: :

if z > a → a := n! fi y := z

R

:

z=a

S1 DO S2

Invariante P : x!∗y = n!

4.

5.

Determinar H2(R) para wp(DO,R) Donde: DO

:

R

:

do i > 3 → i := i − 3 od i=3

Calcular la precondición más débil, wp(S, R) Donde: S S1

: :

S1;DO r := a;x := x − 1

DO R

: :

do r ≥ d → r := r − d;y := x − 1 od (0 ≤ r ≤ d) ∧ (d|(a − r))

Invariante P : d > 0 ∧ d|(a − r) ∧ r ≥ 0 6.

Calcular la precondición más débil, wp(S, R), como se puede notar este es el algoritmo de exponenciación binaria Right-to-Left Donde: S S1 DO

: : :

S1;DO d := 1;x := a;k := b do k > 0 → if ¬(2|k) → k := k − 1;d := x ∗ d; fi; x := x ∗ x;k := k div 2 od

R

:

d = ab

Invariante P: xk * d = ab 7. Calcular la precondición débil de Dijkstra:

wp(x:=x/y ; y:=y+1; abort; x:=x+z,x>z)

8. Calcular la precondición débil de Dijkstra:

wp(x:=3 ; y:=2; x:=x+1; y:=y+3, x>y) 9. Calcular la precondición débil de Dijkstra:

wp(z:=z+1 ;skip; w:=w+1; z:=1; w:=3, z>=w) 10. Calcular la precondición débil de Dijkstra: wp : donde DO :

(DO,R)

R

x=0

:

do x > 0 → x := x-1 od

Considerando: P: x>= 0