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

o Título: Uso de aserciones en la

documentación de programas

o Unidades de contenido

• Especificación de programas
• Representación de valores iniciales y finales

de variables

• Esquemas de prueba

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

2

1

Tema 4: Aserciones

Especificación de programas

Bloque didáctico II:

Semántica de programas

o Especificación

• Describir exactamente que debe efectuar la

ejecución de un programa

o ¿Cómo?

• Lenguaje natural: Comando-comentario
• Ej: Almacenar en z el producto de a*b, asumiendo
que a y b son inicialmente mayores o iguales a cero

• Ej: Multiplicar a y b

•

Inconveniente: Ambiguedad

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

3

Tema 4: Aserciones

Especificación de programas (II)

Bloque didáctico II:

Semántica de programas

o Hoare, 1969

{Q} S {R} ⇒ Especificación de corrección total

•
• Q ⇒ Precondición, aserción de entrada
• R ⇒ Postcondición, aserción de salida
• Si la ejecución de S comienza en un estado que

satisfaga Q, entonces se garantiza su terminación
en un tiempo finito en un estado que satisfaga R

o Ej: {0 £ a 0 £ b} S {R: z = a*b}

• S: z;=0; a;=0; b:=0;
• Fijados a,b ‡ 0, se verifica que R: z = a*b

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

4

2

Tema 4: Aserciones

Especificación de programas (III)

Bloque didáctico II:

Semántica de programas

o Ej: Calcular el sumatorio de un array

• Fijados n ‡ 0 y un array b[0:n-1], establecer

R: (∑ I ˛

[0,n〉: b[I])

o Ej: Ordenar los elementos de un array

• Fijados n ‡ 0 y un array b[0:n-1], ordenar b es

decir R: ("

I ˛

[0,n-1〉: b[I] £ b[I+1])

• Poner todos los elementos de b a cero
⇒ Establecer valores iniciales y finales

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

5

Tema 4: Aserciones

Representación de valores iniciales y finales

Bloque didáctico II:

Semántica de programas

o Programa swap

•

Intercambia los valores de x e y utilizando t

o Formalmente

• Valores iniciales: mayúsculas
• Variables del programa: minúsculas
{x=X
Swap
{R: x=Y

y=Y}

y=X}

Swap:
t := x;
x := y;
y := t;

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

6

3



Tema 4: Aserciones

Bloque didáctico II:

Semántica de programas

Representación de valores iniciales y finales

(II)

o Ej: Ordenación de un array

Fijados n ‡

‡ 0 y un array c[0:n-1] con c=C

establecer
R: perm(C,c)

("
" I ˛

˛ [0,n-1〉〉〉〉:c[I]£

£ c[I+1])

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

7

Tema 4: Aserciones
Esquemas de prueba

Bloque didáctico II:

Semántica de programas

o Predicado entre instrucciones ⇒ Aserción

•

Indica lo que se cumple en ese punto de ejecución

o Programa totalmente

especificado
• Aserciones entre cada par de

y=Y}

instrucciones

o Anotar un programa

• Situar aserciones en él
• ⇒Programa anotado

Swap
{x=X
t := x
{t=X
x := y
{t=X
y := t
{x=Y

x=X

y=Y}

x=Y

y=Y}

y=X}

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

8

4

‡
‡



"
"
˛
˛
£
£



Bloque didáctico II:

Semántica de programas

Tema 4: Aserciones
Esquemas de prueba (II)
{i‡
‡ 0
i:=i+1; s:=s+i
{i>0

s=1+2+...+i}

s=1+2+...+i}

o Ej:

o Convenciones

• Aserción: nombre

seguido de dos puntos
• Aserciones adyacentes
significan que la primera
implica la segunda

{P: i‡
‡ 0
{P1:i+1>0
i:=i+1;
{P2:i>0
{P3:i>0
s:=s+i
{R:i>0

s=1+2+...+i}

s=1+2+...+(i+1-1)}

s=1+2+...+(i-1)}
s+i=1+2+...+(i)}

s=1+2+...+i}

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

9

Tema 4: Aserciones
Esquemas de prueba (III)

Semántica de programas

Bloque didáctico II:

1 {P: i‡
‡ 0
2 {P1:i+1>0
3 i:=i+1;
4 {P2:i>0
5 {P3:i>0
6 s:=s+i
7 {R:i>0

s=1+2+...+i}

s=1+2+...+(i+1-1)}

s=1+2+...+(i-1)}
s+i=1+2+...+(i)}

s=1+2+...+i}

P ⇒⇒⇒⇒ P1
P ⇒⇒⇒⇒ P1
{P1}i:=i+1{P2}
{P1}i:=i+1{P2}
P2 ⇒⇒⇒⇒ P3
P2 ⇒⇒⇒⇒ P3
{P3}s:=s+i{R}

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

10

5

‡
‡



‡
‡



‡
‡



Tema 4: Aserciones
Esquemas de prueba (IV)

Semántica de programas

Bloque didáctico II:

o Escribir la especificación formal para:

• Establecer que x es el valor máximo del array

b[0:n-1]

• Establecer que x es el valor absoluto de x
• Encontrar la posición de un valor máximo del array

b[0:n-1]

• Encontrar la posición del primer valor máximo del

array b[0:n-1]

• Determinar si un entero dado x mayor o igual que

1 es primo

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

11

Tema 4: Aserciones
Esquemas de prueba (V)

Semántica de programas

Bloque didáctico II:

o Escribir la especificación formal para:

• Determinar si un array de enteros b[0:n-1] está

ordenado de forma ascendente

• Colocar en cada posición de un array b[0:n-1] la

suma de los valores de b

• Encontrar la primera persona que está en dos

listas ordenadas alfabéticamente

• Encontrar la primera persona que está en tres

listas ordenadas alfabéticamente

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

12

6