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
Tecnología de la Programación

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

Elena Mª Hernández Pereira
Elena Mª Hernández Pereira

Óscar Fontenla Romero
Óscar Fontenla Romero

Bloque didáctico II: Semántica de programas
Bloque didáctico II: Semántica de programas

Tema 6
Tema 6

: El lenguaje GCL, Guarded
Guarded

oo Título

Título: El lenguaje GCL,
Command Language
Command
Language
Unidades de contenido
oo Unidades de contenido
•• Los comandos
Los comandos skipskip, , abort
•• El comando asignación
El comando asignación
La estructura alternativa
•• La estructura alternativa
•• La estructura iterativa
La estructura iterativa
•• Funciones y procedimientos
Funciones y procedimientos

abort y composición
y composición

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

22

1

Bloque didáctico II:

Semántica de programas

oo GCL:

Guarded Command Language [Dijkstra, 1976]
[Dijkstra, 1976]

Tema 6: GCL
Tema 6: GCL
Introducción
Introducción
GCL: Guarded Command Language
Sintaxis simple y muy reducida
•• Sintaxis simple y muy reducida
Más cómodo para realizar demostraciones formales
•• Más cómodo para realizar demostraciones formales
•• Permite
Permite asignaciones simultáneas
oo Semántica operacional
Semántica operacional
Funcionamiento de cada instrucción
Funcionamiento de cada instrucción
••
estado, instrucción〉〉 fi
Relación 〈〈estado, instrucción
•• Relación
{ (x,1), (y,2) }, “x := 0” 〉〉 fi
•• Ej: Ej: 〈〈 { (x,1), (y,2) }, “x := 0”
Semántica axiomática
oo Semántica axiomática
Caracterización (definción)
•• Caracterización (definción)
•• En términos del predicado
En términos del predicado wpwp

asignaciones simultáneas y y no determinismo
no determinismo

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

estado
estado

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

33

Bloque didáctico II:

Semántica de programas

Tema 6: GCL
Tema 6: GCL

Sintaxis
Sintaxis

oo

Instrucciones
Instrucciones
skipskip
1.1.
abort
2.2. abort
Composición secuencial S11;S;S22
3.3. Composición secuencial S
:= a
4.4. Asignación simple x
Asignación simple x11 :=
Asignación múltiple x11, x, x22, …,
5.5. Asignación múltiple x
Instrucción condicional ifif BB11 fi
Instrucción condicional
Instrucción iterativa do B11 fi
Instrucción iterativa do B

6.6.

7.7.

11, , a

11
:= a
, …, xxmm :=
SS11 |…|…BBmm fi
SS11 |…|…BBmm fi

mm

, …,a
22, …,
SSmm fifi
SSmm odod

donde m ‡
donde m
BBii fórmulas (sin cuantificadores) y S

0, x0, xii variables o referencias a

fórmulas (sin cuantificadores) y Sii instrucciones
instrucciones

arrays, , a
variables o referencias a arrays

i i expresiones,
expresiones,

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

44

2

fi
fi
a
a
a
a
fi
fi
fi
fi
‡
a
Bloque didáctico II:

Semántica de programas

Tema 6: GCL
Tema 6: GCL
skipskipy y abortabort

oo skipskip

Transformación identidad
•• Transformación identidad
s, “skip”〉〉 fi
ss
〈〈s, “skip”
••
•• wp(skip,R) = R
wp(skip,R) = R
oo abort
abort
s, “abort”〉〉 fi
〈〈s, “abort”
••
wp(abort,R) = F
•• wp(abort,R) = F
•• No existe ningún estado de partida que garantice
No existe ningún estado de partida que garantice
que dicho comando termina en un estado definido
que dicho comando termina en un estado definido
y útil
y útil

s’ para cualquier s y s’
s’ para cualquier s y s’

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

55

Tema 6: GCL
Tema 6: GCL

Composición secuencial
Composición secuencial

Bloque didáctico II:

Semántica de programas

oo SS11;S;S22

〈〈s, (Ss, (S11;S;S22))〉〉 fi

s’ s’

〈〈s, Ss, S11〉〉 fi
”,R) = wp(S11,wp(S

••
•• wp(“Swp(“S11;S;S22”,R) = wp(S
Es asociativa
•• Es asociativa
 wp(“Swp(“S11;(S;(S22;S;S33)”,R) = wp(“(S

s’’ y 〈〈s’’, Ss’’, S22〉〉 fi
s’’ y
,wp(S22,R))
,R))

s’ s’

)”,R) = wp(“(S11;S;S22);S);S33”,R)
”,R)

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

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

66

3

fi
fi
fi

fi
fi
Bloque didáctico II:

Semántica de programas

Tema 6: GCL
Tema 6: GCL

Comando asignación
Comando asignación
oo Asignación simple a variables simples
Asignación simple a variables simples

oo Asignación múltiple a variables simples
Asignación múltiple a variables simples

oo Asignación a un elemento de un array
Asignación a un elemento de un array

oo Asignación múltiple general
Asignación múltiple general

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

77

Tema 6: GCL
Tema 6: GCL

Bloque didáctico II:

Semántica de programas

Asignación simple a variables simples
Asignación simple a variables simples
x := aa
x :=

oo

expresión, ambas del mismo tipo
expresión, ambas del mismo tipo

(s; x:s(a
(s; x:s(

)) siempre que s(a
)) siempre que s(

) ) ˛

rango(x)
rango(x)

““〉〉 fi
”,R) = dominio(a
”,R) = dominio(

x variable simple, a
x variable simple,
••
El identificador x toma el valor de la expresión aa
•• El identificador x toma el valor de la expresión
s, “x := a
〈〈s, “x :=
••
wp(“x:= a
•• wp(“x:=
Ejemplos
oo Ejemplos
Dados x,y:integer y s={ (x,1), (y,2) }:
•• Dados x,y:integer y s={ (x,1), (y,2) }:
s, “y := x--1“1“〉〉 fi
〈〈s, “y := x
••
s, “x := y; skip; y := y--1“1“〉〉 fi
〈〈s, “x := y; skip; y := y
s, “skip; abort“〉〉 fi
〈〈s, “skip; abort“

no existe estado siguiente
no existe estado siguiente

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

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

) cand R
) cand Rxxa

••

••

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

88

4

a
a
fi
a
a
˛
a
a
a
fi
fi
fi
Tema 6: GCL
Tema 6: GCL

Asignación simple a variables simples
Asignación simple a variables simples

Bloque didáctico II:

Semántica de programas

Ejemplos
oo 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)
wp(“x:=5”,x„
•• wp(“x:=5”,x
dominio(5) cand F = F
dominio(5) cand F = F
Para cualquier predicado pp de un argumento
de un argumento
wp(“x:=a/b”,p(x)) = dominio(a/b) cand (p(x)
wp(“x:=a/b”,p(x)) = dominio(a/b) cand (p(x)xx
= ((b „
= ((b

„ 5) = dominio(5) cand (5
5) = dominio(5) cand (5 „

•• Para cualquier predicado

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

5) =
5) =

a/ba/b)
)

oo Ausencia de efectos colaterales
Ausencia de efectos colaterales

Dados x,y distintos y una constante C,
 Dados x,y distintos y una constante C,
wp(“x:=e”, y=C) = (y=C)
wp(“x:=e”, y=C) = (y=C)

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

99

Tema 6: GCL
Tema 6: GCL

Asignación simple a variables simples
Asignación simple a variables simples

Bloque didáctico II:

Semántica de programas

Dada una secuencia de instrucciones
oo Dada una secuencia de instrucciones
wp(“Swp(“S11;S;S22;S;S33;S;S44”,R)
”,R)
”,wp(“S44”,R))
= wp(“S
= wp(“S11;S;S22;S;S33”,wp(“S
”,R))
= wp(“S
= wp(“S11;S;S22”,wp(“S
”,wp(“S33”,wp(“S
= wp(“S
= wp(“S11”,wp(“S
Lo simplificamos como
Lo simplificamos como

”,wp(“S44”,R)))
”,R)))
”,wp(“S33”,wp(“S

”,wp(“S22”,wp(“S

”,wp(“S44”,R))))
”,R))))

oo

••

••

{wp{wp11} S} S11 {wp{wp22} S} S22 {wp{wp33} S} S33 {wp{wp44} S} S44 {R}
{R}
{wp{wp11} S} S11;S;S22;S;S33;S;S4 4 {R}
{R}

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

1010

5

„
„
Tema 6: GCL
Tema 6: GCL

Bloque didáctico II:

Semántica de programas

Asignación simple a variables simples
Asignación simple a variables simples

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

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

1111

Tema 6: GCL
Tema 6: GCL

Bloque didáctico II:

Semántica de programas

Asignación múltiple a variables simples
Asignación múltiple a variables simples

oo

••

••

xx11, …,

:= aa 11,…,

,…,aa nn ⇒⇒‘‘ x x :=
:= ‘a‘a
, …, xxnn :=
variables simples distintas, a
xxii variables simples distintas,
:= a
〈〈s, “xs, “x11,…,
,…, xxnn :=
siempre que s(a
siempre que s(

,…,a
11,…,
ii) ) ˛

nn““〉〉 fi

rango(x
rango(xii))
“,R) = dominio(‘
“,R) = dominio(

•• wpwp(“(“‘

‘ x = x = ‘

donde dominio(‘
donde dominio(

) = ("
) = (

ii expresiones
expresiones

(s; x11:s(:s(a
(s; x

);…;xxnn:s:s((a
11);…;

nn)) ))

) ) cand
I : dominio(a
I : dominio(

cand RRxxa
ii)) ))

Ejecución
oo Ejecución
Se evalúan las a
•• Se evalúan las
Se asigna v11 a xa x11, …,
•• Se asigna v

ii en cualquier orden para obtener v
en cualquier orden para obtener vi i
, …, vvnn a a xxnn en este orden
en este orden

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

1212

6

a
a
a
fi
a
a
a
˛
a
‘
a
a
‘
a
a
a
‘
a
"
a
a
Tema 6: GCL
Tema 6: GCL

Bloque didáctico II:

Semántica de programas

Asignación múltiple a variables simples
Asignación múltiple a variables simples

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