Tema 6 - QueGrande.orgquegrande.org/apuntes/ETIS/2/TP/teoria/07-08/tema_6.pdfTema 6: GCL Asignación...

1

Tecnología de la Programación

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

Elena Mª Hernández PereiraÓscar Fontenla Romero

UNIVERSIDAD DE A CORUÑAFACULTAD DE INFORMÁTICA

DEPARTAMENTO DE COMPUTACIÓN

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

Bloque didáctico II: Semántica de programas

Tema 6o Título: El lenguaje GCL, Guarded

Command Languageo Unidades de contenido

• Los comandos skip, abort y composición• El comando asignación• La estructura alternativa• La estructura iterativa• Llamadas a procedimientos

2


Tema 6: GCLIntroducción

o GCL: Guarded Command Language [Dijkstra, 1976]

• Sintaxis simple y muy reducida• Más cómodo para realizar demostraciones formales• Permite asignaciones simultáneas y no determinismo

o Semántica operacional• Funcionamiento de cada instrucción• Relación ⟨estado, instrucción⟩ → estado• Ej: ⟨ { (x,1), (y,2) }, “x := 0” ⟩ → { (x,0), (y,2) }

o Semántica axiomática• Caracterización (definción)• En términos del predicado wp



Tema 6: GCLSintaxis

o Instrucciones1. skip2. abort3. Composición secuencial S1;S2

4. Asignación simple x1 := α5. Asignación múltiple x1, x2, …, xm := α1, α2, …,αm

6. Instrucción condicional if B1 → S1 |…Bm → Sm fi7. Instrucción iterativa do B1 → S1 |…Bm → Sm od

donde m ≥ 0, xi variables o referencias a arrays, αi expresiones, Bi fórmulas (sin cuantificadores) y Si instrucciones


3


Tema 6: GCLskip y abort

o skip• Transformación identidad• ⟨s, “skip”⟩ → s• wp(skip,R) = R

o abort• ⟨s, “abort”⟩ → s’ para cualquier s y s’• wp(abort,R) = F• No existe ningún estado de partida que garantice

que dicho comando termina en un estado definido y útil



Tema 6: GCLComposición secuencial

o S1;S2

• ⟨s, (S1;S2)⟩ → s’ ⇔ ⟨s, S1⟩ → s’’ y ⟨s’’, S2⟩ → s’• wp(“S1;S2”,R) = wp(S1,wp(S2,R))• Es asociativa

� wp(“S1;(S2;S3)”,R) = wp(“(S1;S2);S3”,R)

o Ejemplos:• wp(“skip;skip”,R)

= wp(skip,wp(skip,R)) = wp(skip,R) = R• wp(“S;abort”,R) = F


4


Tema 6: GCLComando asignación

o Asignación simple a variables simples

o Asignación múltiple a variables simples

o Asignación a un elemento de un array

o Asignación múltiple general



Tema 6: GCLAsignación simple a variables simples


o x := α• x variable simple, α expresión, ambas del mismo tipo• El identificador x toma el valor de la expresión α• ⟨s, “x := α“⟩ → (s; x:s(α)) siempre que s(α) ∈ rango(x)• wp(“x:= α”,R) = dominio(α) cand Rx

α

o Ejemplos• Dados x,y:integer y s={ (x,1), (y,2) }: • ⟨s, “y := x-1“⟩ → { (x,1), (y,0) }• ⟨s, “x := y; skip; y := y-1“⟩ → { (x,2), (y,1) }• ⟨s, “skip; abort“⟩ → no existe estado siguiente

5




o Ejemplos• wp(“x:=5”,x=5) = dominio(5) cand (5=5) = dominio(5)

• wp(“x:=5”,x≠5) = dominio(5) cand (5 ≠ 5) = dominio(5) cand F = F

• Para cualquier predicado p de un argumento wp(“x:=a/b”,p(x)) = dominio(a/b) cand (p(x)x

a/b) = ((b ≠ 0) cand p(a/b))

o Ausencia de efectos colaterales� Dados x,y distintos y una constante C,

wp(“x:=e”, y=C) = (y=C)



o Dada una secuencia de instruccioneswp(“S1;S2;S3;S4”,R)= wp(“S1;S2;S3”,wp(“S4”,R))= wp(“S1;S2”,wp(“S3”,wp(“S4”,R)))= wp(“S1”,wp(“S2”,wp(“S3”,wp(“S4”,R))))

o Lo simplificamos como• {wp1} S1 {wp2} S2 {wp3} S3 {wp4} S4 {R}• {wp1} S1;S2;S3;S4 {R}


6



o Ejercicios: Determina y simplifica wp(S,R)



Tema 6: GCLAsignación múltiple a variables simples


o x1, …, xn := α1,…,αn ⇒ x = α• xi variables simples distintas, αi expresiones• ⟨s, “x1,…, xn := α1,…,αn“⟩ → (s; x1:s(α1);…;xn:s(αn))

siempre que s(αi) ∈ rango(xi)• wp(“x = α “,R) = dominio(α ) cand Rx

αdonde dominio(α ) = (∀I : dominio(αi))

o Ejecución• Se evalúan las αi en cualquier orden para obtener vi

• Se asigna v1 a x1, …, vn a xn en este orden

7



o Ejemplos• Dados x,y:integer y s={ (x,1), (y,2) }:

• ⟨s, “x := y; y := x“⟩ → { (x,2), (y,2) }• ⟨s, “x,y := y,x”⟩ → { (x,2), (y,1) }• ⟨s, “x,y,x := y,x,x-1”⟩ → { (x,0), (y,1) }• ⟨s, “x,y := 0,y/x”⟩ → { (x,0), (y,2) }

o Ejercicios• wp(“z,y:=z*x,y-1”,((y ≥ 0) ∧ (z*xy =c)))• wp(“s,i:=s+b[i],i+1”,((i > 0) ∧ s=(∑ J ∈ [0,i ⟩: b[J])))






8



o Utilidad: Derivación de programas

o Dado b:array, i,m,p:integer con i ≤ m < i+p• i, (i+p-1) límites de una partición de p• m índice de esa partición• Se pretende hacer más pequeña la partición

haciendo i = m+1 sin cambiar p• ¿Qué valor se asigna a p?

o Dado: { T } a:= a+1; b:= x { a= b }• Encontrar un valor para x






9


Tema 6: GCLAsignación a un elemento de un array


o Recordamos• Array: variable simple que contiene una función

• b[i] ⇒ aplicación de la función b sobre el argumento i• (b; i : α) ⇒ función igual a b excepto en el argumento

i que produce el valor α• b[i] := α ≡ b := (b; i : α)

o b := (b; i : α)




o b := (b; i : α)• Dado un selector σ = [e1][e2]…[en] donde cada ei son

expresiones, definimos su evaluación en s� s(σ) = [s(e1)] [s(e2)]… [s(en)]

• La ejecución de xσ := α produce el efecto:• ⟨ s, “xσ := α” ⟩ → (s; x: (s(x); s(σ):s(α)))

siempre que ei ∈ dominioi(x) y α ∈ rango(x)

• Tanto α como σ se evalúan en el estado s

10




o Ejemplos:• Dado b[0:2]:integer y s = { (i,1), (b, (0,1,20)) }

• ⟨ s, “b[i+1] := b[b[i]] + 6” ⟩ → { (i,1), (b, (0,1,7)) }

• ⟨ s, “b[b[i-1]] := 7” ⟩ → { (i,1), (b, (7,1,20)) }

• ⟨ s, “b[i+2] := 7” ⟩ → no hay estado siguiente




o b := (b; i : α)• wp(“b[i] := α”,R) = wp(“b := (b; i:α)”,R)

= dominio((b; i:α)) cand Rb(b; i:α)

= enrango(i,b) cand dominio(α) cand Rb(b; i:α)

o Ejemplos:• wp(“b[i] := 5”, b[i]=5)• wp(“b[i] := 5”, b[i]=b[j])• wp(“b[b[i]] := i”, b[i]=i)• wp(“b[n] := x”, ordenado(b[1:n]))

11






Tema 6: GCLAsignación múltiple general


o x1σ1,…, xn σn := α1,…,αn ⇒ xσ = α• xi identificadores, σi selectores y αi expresiones del

mismo tipo que xiσi

• ⟨ s, “x1σ1,…,xnσn := α1,…,αn“ ⟩ →(s; x1: (s(x1); s(σ1):s(α1)); …; xn: (s(xn); s(σn):s(αn))) siempre que σi ∈ dominioi(x) y αi ∈ rango(xi)

• wp(“xσ = α ,R)= dominio(α ) cand Rxσα = Rxσ

α

o Ejecución1. Se evalúan todos los σi en s2. Se evalúan todas las αi en s3. Se asigna de izquierda a derecha

12




o Problema: • Redefinir la sustitución textual ya quexσ no son

sólo identificadores

o Dos casos:• b1σ1,…, bn σn := α1,…,αn asigna primero α1 a b1σ1,

después α2,…,a b2σ2 y así sucesivamente, por lo tanto es equivalente a b := (b; σ1: α1; …;σn: αn)

• Sean b,c identificadores distintos y σ, ρ dos selectores, entonces bσ, cρ := α,β debe tener el mismo efecto que cρ, bσ :=β,α



o Definición Pxα

1. x , lista de identificadores distintos y todos los selectores son ε, entonces tenemos la sustitución textual ya definida

2. Parejas adyacentes de ref-expr se pueden permutar siempre que comiencen por identificadores distintos

3. Asignaciones múltiples a partes de un objeto b pueden verse como una única asignación a b

ybcxfh

ycbxhf

RR ,,,,,,

,,,,,,

οσορβα

οροσβα =


xbgssb

xsbsb

g mm

mm

mRR ,

),:;...;:;(

,,...,

,,..., 11

11

1 ααοο

αα =

13






Tema 6: GCLEstructura alternativa

o Instrucción condicional

o If B1 → S1 | B2 → S2| … | Bn → Sn fi• n ≥ 0• Si instrucciones• Bi predicados booleanos, condiciones o custodias

(guardianes)

o Abreviaturas: • IF• BB ≡ B1 ∨ … ∨ Bn

14



o ⟨ s, IF ⟩ → s’ se da siempre que:• ¬ ∃ Bi tal que s(Bi) = U• s’ es un estado tal que para una rama i, s(Bi) = T y ⟨s, Si⟩ → s’

o Es decir,• Si ∃ Bi tal que s(Bi) = U, aborta• Si ¬ ∃ Bi tal que s(Bi) = T, aborta• Toma un Bi cualquiera que sea cierto y ejecuta Si



o Ejemplo• S1 = { (a,1), (b,0), (x,0) }• S2 = { (a,0), (b,1), (x,0) }• S3 = { (a,2), (b,1), (x,0) }• S4 = { (a,1), (b,1), (x,0) }

o Sirve de if-then-else y de caseo No tiene rama default ni sentencia if-theno Ejemplo:

• if x<0 then x:=abs(x);

if a = 1 →→→→ x:=1| a/b > 0 →→→→ x:=2| a/b < 0 →→→→ x:=3fi

if x < 0 →→→→ x:=abs(x)| x ≥≥≥≥ 0 →→→→ skipfi

15



o wp(IF, R) = dominio (BB) ∧ BB ∧ (B1 ⇒ wp(S1, R)) ∧ …∧ (Bn ⇒ wp(Sn, R))

o wp(IF, R) = (∃ I ∈ [1,n]: B1) ∧ (∀ I ∈ [1,n]: BI ⇒ wp(SI, R))

o Ejemplos:• Programa que deja en x el valor absoluto de z• Programa que cuenta el número de valores positivos

de un array b[0:n-1]



o Teorema:

o Probar que Q ⇒ wp(IF, R) equivale a probar: • Q ⇒ dominio (BB)• Q ⇒ BB• Q ∧ BI ⇒ wp(SI, R) ∀i ∈ [1:n]

16


Tema 6: GCLEstructura repetitiva

o Instrucción iterativa

o do B1 → S1 | B2 → S2| … | Bn → Sn od• n ≥ 0• Si instrucciones• Bi predicados booleanos, condiciones o custodias

(guardianes)

o Abreviaturas: • DO• BB ≡ B1 ∨ … ∨ Bn



o ⟨ s, DO ⟩ → s’ se da siempre que:• ¬ ∃ Bi tal que s(Bi) = U• s’ es un estado tal que

� ∃ i, s(Bi) = T y ⟨s, (Si:DO)⟩ → s’� ∀ i, s(Bi) = F y s’ = s

o Es decir,• Si ∃ Bi tal que s(Bi) = U, aborta• Si ¬ ∃ Bi tal que s(Bi) = T, finaliza en el estado s• Toma un Bi cualquiera que sea cierto y ejecuta Si y en

el estado resultante vuelve a ejecutar DO

17



o DO en función de IF• do BB → if B1 → S1 | … | Bn → Sn fi od

o Ejemplo:• En s = { (i,6) }, s’ = { (i,3) } ejecutar los

siguientes programas

do i/abs(i)= 1 →→→→ i:=i-2| i/abs(i)= -1 →→→→ i:=i+2od

do i ≠≠≠≠ 0 cand i/abs(i)= 1 →→→→ i:=i-2| i ≠≠≠≠ 0 cand i/abs(i)= -1 →→→→ i:=i+2od



o wp(DO, R) • Acabar en 0 iteraciones

� H0(R) = ¬ BB ∧ R• Acabar en k > 0 iteraciones

� Hk(R) = wp(IF,Hk-1(R))• Acabar en cualquier número de iteraciones

� wp(DO,R) = (∃ k: 0 ≤ k: wp(IF,Hk(R)))

o Problema: • No es aplicable en la práctica• El desarrollo de wp(DO,R) es recursivo y puede ser

que nunca terminemos de elaborarlo

18



o Técnica:(1) Para demostrar corrección parcial

• Buscamos una fórmula, llamada invariante, cierta antes y después de toda iteración del bucle (incluso al terminar)

(2) Para demostrar que el bucle finaliza• Buscamos una función t, llamada función

cota, que en cada iteración sea positiva y decreciente



o Ejemplo:

o Ejemplo: { b ≥≥≥≥ 0}x, y, z:= a, b, 0;do y > 0 ∧∧∧∧ par(y) →→→→ y, x:= y/2, x+x

| impar(y) →→→→ y, z:= y-1, z+xod{R: z = a*b}

i, s := 1, b[0];do i < 11 →→→→ i, s :=i+1, s+ b[i] od{R: s = ( ∑∑∑∑K ∈∈∈∈[0,11 ⟩⟩⟩⟩: b[K])}

19



o TeoremaDados DO, P y t tales que:

(1) P ∧ Bi ⇒ wp(Si,P) ∀i ∈[1,n](2) P ∧ BB ⇒ t > 0(3) P ∧ Bi ⇒ wp(“t1:=t; S”,t < t1) ∀i ∈[1,n]Entonces P ⇒ wp(DO, P ∧ ¬BB)



o Método de prueba(1) P es cierto justo antes

de comenzar el bucle

(2) {P ∧ Bi} Si {P} para cada rama

(3) P ∧ ¬BB ⇒ R(4) P ∧ BB ⇒ t > 0(5) {P ∧ Bi } t1:=t; Si {t < t1}

{ Q: … }{ inv P: … }{ cota t: … }do B 1 →→→→ S1

| …| B n →→→→ Sn

od{R: …}

20


Tema 6: GCLFunciones y procedimientos

o

o Ejemplos func abs(x:integer) ret (a:integer)if x ≤ 0 → a:= -x| x > 0 → a:= xfi

func fact(i:integer) ret (f:integer)if i = 0 → f:= 1| i > 0 → f:= fact(i-1)*ifi

}resultadoparametros

nn trtvtvf ):(ret ):;...;:( func 11

44 844 76



o

o Ejemplos proc swap( var i,j:integer)i,j := j,i

proc div(n,d:integer; var c,r:integer)c,r := 0,n;do r ≥ d → c,r := c+1,r-dod

44 844 7644 844 76referencia

mm

valor

nn tvtvtvtvp ):;...;: var ;:;...;:( proc '''1

'111

21



o Ejercicios• Dado un número x, devolver la primera posición i

en un array b[0:n-1] tal que b[i] ≥ x.• Insertar un elemento x en un array b[0:n-1]

ordenado desde 0 a n-2.• Programar el procedimiento div(n,d,c,r) de modo

recursivo.

• Escribir una función recursiva para el máximo común divisor mcd(a,b).



o Funciones

o Por simplicidad, supondremos que• En Q sólo aparecen libres lasX• En R sólo aparecen libres lasX y r• Las variables internas de f no se usan en el

resto del programa

func f( X) ret r{Q} S {R}

22


Tema 6: GCLFunciones

o Ejemplo

o Las llamadas tienen la forma yσ := α(f(e)) donde:• e son expresiones del mismo tipo que X• yσ coincide en tipo con r• α(f( e)) es una expresión que contiene a f(e) una sóla vez• f no aparece en σ ni en e

func abs(X) ret r{Q: T}if X ≥ 0 → r:= X| x ≤ 0 → r:= -Xfi{R: (X ≥ 0 ∧ r=X) ∨ (X ≤ 0 ∧ r=-X)}



o Ejemplo de llamadas posibles• y := abs(10 - a*2);• b[0] := abs(b[1] - b[2])• y := abs(a) + 1

o Se descartan llamadas del tipo• z := abs( abs(x) – z)• b[abs(i - j)] := 0

o Que pueden ser sustituidas por asignaciones intermedias• aux 0 := abs(a); z := abs(aux 0 – z)• aux 1 :=abs(i – j); b[aux 1] := 0;

23



o La llamada y:=f(e) equivale a ejecutar• X := e; S; y := α (r)

o Supongamos que hemos demostrado {Q} S {R}. Para demostrar:• {G} y := α(f(e)) {H}

o debemos realizar los siguientes pasos:• (1) G ⇒ Q X

e

• (2) G ∧ R X e ⇒ Hy

α(r)

o Ejemplo: Demostrar• {a > b ∧ c > 0} b:= c * abs(a – b) {b > 0}


Tema 6: GCLProcedimientos

o Procedimientos

o Por simplicidad, supondremos que• En Q sólo aparecen libres las X• En R sólo aparecen libres las X y r• Las variables internas de p no se usan en el resto del

programa• Las variables r funcionan por copia local. Es decir, la

llamada p(e,y) equivale a:� X,r := e,y; S; y := r

proc p( X; var r){Q} S {R}

24


Tema 6: GCLProcedimientos

o Ejemplo

o Supongamos que hemos demostrado {Q} S {R}. Para demostrar • {G} p(e, y) {H}

o debemos realizar los siguientes pasos:• (1) G ⇒ Qx,r

e,y

• (2) G ∧ RXe ⇒ Hy

r

o Ejemplo: Demostrar {a ≥0 ∧ b=B} incr(a+1,b) {b > B}

proc incr(X; var r){Q: r = Z}

r := r + X;{R: r = Z + X}


Tema 6: GCLRecursividad

o Definición• La función (o procedimiento) f es recursiva si su

ejecución puede producir una nueva llamada a f

o Ejemplo

o Recursividad directa: la llamada a f se produce en el cuerpo de f. • Ejemplo: fact

func fact(X) ret rif X = 0 → r := 1| X > 0 → r := X * fact(X – 1)fi

25


Tema 6: GCLRecursividad

o Recursividad indirecta: f llama a otra función g cuya ejecución acaba finalmente llamando a f de vuelta. • Ejemplo: func par(X) ret r:boolean

if X = 0 → r := T| X > 0 → r := impar(X – 1)fi

func impar(X) ret r:booleanif X = 0 → r := F| X > 0 → r := par(X – 1)fi


Tema 6: GCLRecursividad directa

o Simple o lineal: cada ejecución del cuerpo de fgenera como mucho una nueva llamada a f (a primer nivel). • Ejemplo: fact

o Múltiple o no lineal: ejecutar el cuerpo de fpuede suponer hacer uso de f dos o más veces.• Ejemplo: func fibo(X) ret r

if X = 0 → r := 0| X = 1 → r := 1| X > 1 → a := fibo(X – 1);

b := fibo(X – 2);r := a + b

fi

26


Tema 6: GCLRecursividad directa lineal

o Final: la llamada es la última instrucción ejecutada. • Ejemplo: fact

o Ejemplo de No final:func max(B[0:N-1],i,d) ret rif i < d → r := max(B,i+1,d)| i = d → r := B[i]fi;if B[i] > r → r := B[i]| B[i] ≤ r → skipfi

Tema 6 - QueGrande.orgquegrande.org/apuntes/ETIS/2/TP/teoria/07-08/tema_6.pdfTema 6: GCL Asignación...

Documents

Transcript of Tema 6 - QueGrande.orgquegrande.org/apuntes/ETIS/2/TP/teoria/07-08/tema_6.pdfTema 6: GCL Asignación...