PDF de programación - Tema 6 - 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 6

o Título: El lenguaje GCL, Guarded

Command Language

o Unidades de contenido

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

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

2

1

Bloque didáctico II:

Semántica de programas

Tema 6: GCL
Introducció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〉 fi
• Ej: 〈 { (x,1), (y,2) }, “x := 0” 〉 fi

estado

{ (x,0), (y,2) }

o Semántica axiomática

• Caracterización (definción)
• En términos del predicado wp

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

3

Bloque didáctico II:

Semántica de programas

Tema 6: GCL

Sintaxis

o

Instrucciones

skip
1.
2. abort
3. Composición secuencial S1;S2
4. Asignación simple x1 := a
5. Asignación múltiple x1, x2, …, xm := a
fi S1 |…Bm
fi S1 |…Bm

Instrucción condicional if B1
Instrucción iterativa do B1

6.

7.

1, a
2, …,a
fi Sm fi
fi Sm od

m

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

i expresiones,

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

4

2

Bloque didáctico II:

Semántica de programas

Tema 6: GCL
skipy abort

o skip

• Transformación identidad
s
•
• wp(skip,R) = R

〈s, “skip”〉 fi

o abort

〈s, “abort”〉 fi

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

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

5

Tema 6: GCL

Composición secuencial

Bloque didáctico II:

Semántica de programas

o S1;S2

s’’ y 〈s’’, S2〉 fi

s’

s’

〈s, (S1;S2)〉 fi

•
• wp(“S1;S2”,R) = wp(S1,wp(S2,R))
• Es asociativa

〈s, S1〉 fi

 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

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

6

3

Bloque didáctico II:

Semántica de programas

Tema 6: GCL

Comando 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

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

7

Tema 6: GCL

Bloque didáctico II:

Semántica de programas

Asignación simple a variables simples
x := a

o

x variable simple, a expresión, ambas del mismo tipo

•
• El identificador x toma el valor de la expresión a
•

(s; x:s(a )) siempre que s(a ) ˛

〈s, “x := a “〉 fi

rango(x)

• wp(“x:= a ”,R) = dominio(a ) cand Rxa

o Ejemplos

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

{ (x,1), (y,0) }

〈s, “y := x-1“〉 fi
〈s, “x := y; skip; y := y-1“〉 fi
〈s, “skip; abort“〉 fi

•

•

{ (x,2), (y,1) }

no existe estado siguiente

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

8

4

Tema 6: GCL

Asignación simple a variables simples

Bloque didáctico II:

Semántica de programas

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
= ((b „ 0) cand p(a/b))

a/b)

o Ausencia de efectos colaterales

 Dados x,y distintos y una constante C,

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

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

9

Tema 6: GCL

Asignación simple a variables simples

Bloque didáctico II:

Semántica de programas

o Dada una secuencia de instrucciones

wp(“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))))
Lo simplificamos como

o

•

•

{wp1} S1 {wp2} S2 {wp3} S3 {wp4} S4 {R}
{wp1} S1;S2;S3;S4 {R}

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

10

5

Tema 6: GCL

Bloque didáctico II:

Semántica de programas

Asignación simple a variables simples

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

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

11

Tema 6: GCL

Bloque didáctico II:

Semántica de programas

Asignación múltiple a variables simples

o

•

•

x1, …, xn := a 1,…,a n ⇒‘x = ‘a
xi variables simples distintas, a
〈s, “x1,…, xn := a
siempre que s(a

1,…,a
i) ˛

n“〉 fi

rango(xi)
“,R) = dominio(‘

• wp(“‘ x = ‘

donde dominio(‘

) = ("

i expresiones

(s; x1:s(a

1);…;xn:s(a

n))

I : dominio(a

) cand Rxa
i))

o Ejecución

• Se evalúan las a
• Se asigna v1 a x1, …, vn a xn en este orden

i en cualquier orden para obtener vi

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

12

6

a
a
a
Tema 6: GCL

Bloque didáctico II:

Semántica de programas

Asignación múltiple a variables simples

o Ejemplos

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

〈s, “x := y; y := x“〉 fi
〈s, “x,y := y,x”〉 fi
〈s, “x,y,x := y,x,x-1”〉 fi
〈s, “x,y := 0,y/x”〉 fi

•

•

•

•

{ (x,2), (y,2) }

{ (x,2), (y,1) }

{ (x,0), (y,1) }

{ (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])))

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

13

Tema 6: GCL

Bloque didáctico II:

Semántica de programas

Asignación múltiple a variables simples

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

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

14

7

Tema 6: GCL

Bloque didáctico II:

Semántica de programas

Asignación múltiple a variables simples

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

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

15

Tema 6: GCL

Bloque didáctico II:

Semántica de programas

Asignación múltiple a variables simples
o Ejercicios: Determina y simplifica wp(S,R)

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

16

8

Tema 6: GCL

Bloque didáctico II:

Semántica de programas

Asignació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 : a ) ⇒ función igual a b excepto en el argumento
i que produce el valor a
b[i] := a
b := (b; i : a )

b := (b; i : a )

o

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

17

Tema 6: GCL

Bloque didáctico II:

Semántica de programas

Asignación a un elemento de un array
b := (b; i : a )
• Dado un selector s = [e1][e2]…[en] donde cada ei son

expresiones, definimos su evaluación en s

o



s(s ) = [s(e1)] [s(e2)]… [s(en)]

La ejecución de xs
〈 s, “xs
:= a ” 〉 fi
siempre que ei

:= a produce el efecto:

(s; x: (s(x); s(s ):s(a )))
˛ dominioi(x) y a

rango(x)

Tanto a como s se evalúan en el estado s

•

•

•

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

18

9

”
˛
Tema 6: GCL

Bloque didáctico II:

Semántica de programas

Asignación a un elemento de un array

o Ejemplos:

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

〈 s, “b[i+1] := b[b[i]] + 6” 〉 fi

{ (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

•

•

•

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

19

Tema 6: GCL

Bloque didáctico II:

Semántica de programas

o

Asignación a un elemento de un array
b := (b; i : a )
• wp(“b[i] := a ”,R) = wp(“b := (b; i:a )”,R)
(b; i:a )

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

(b; i:a )

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]))

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

20

10

fi
fi
Tema 6: GCL

Bloque didáctico II:

Semántica de programas

Asignación a un elemento de un array

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

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

21

Tema 6: GCL

Bloque didáctico II:

Semántica de programas

Asignación múltiple general

o

•

•

x1s 1,…, xn s n := a 1,…,a n ⇒‘‘ xs = ‘a

xi identificadores, s
mismo tipo que xi
n := a
n“ 〉 fi
〈 s, “x1
1,…,xn
(s; x1: (s(x1); s(s
1):s(a
˛ dominioi(x) y a
siempre que s
i
,R)= dominio(‘
• wp(“‘xs = ‘a

i selectores y a
1,…,a
1)); …; xn: (s(xn); s(s

) cand Rxs

i

i expresiones del

n):s(a
rango(xi)

a = Rxs

i

n)))

o Ejecución

1. Se evalúan todos los s
2. Se evalúan todas las a
3. Se asigna de izquierda a derecha

i en s
i en s

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

22

11

s
s
s
˛
a
a
Tema 6: GCL

Bloque didáctico II:

Semántica de programas

Asignación múltiple general

o Problema:

• Redefinir la sustitución textual ya que‘xs no son

sólo identificadores

•

o Dos casos:
s
b1
1,…, bn
después a
tanto es equivalente a b := (b; s

s
1 a b1
n: a
• Sean b,c identificadores distintos y s , r dos

n := a
s
1,…,a
s
2,…,a b2

1,
2 y así sucesivamente, por lo

n asigna primero a
1; …;s

1: a

n)

selectores, entonces bs , cr := a ,b debe tener el
mismo efecto que