PDF de programación - Seminario de especificaciones algegraicas

Algoritmos y Estructuras de Datos

Ingeniería en Informática, Curso 2º, Año 2003/2004



SEMINARIO DE

ESPECIFICACIONES ALGEBRAICAS



Contenidos:

1. Descripción general de Maude
2. Comandos básicos
3. Formato de especificación
4. Ejemplos
Ejercicios



OJO: Antes de hacer esta práctica repasar las especificaciones algebraicas o
axiomáticas (Tema 1 de la Parte 1 de la asignatura).

Algoritmos y Estructuras de Datos, 2003/2004
Seminario de Especificaciones Algebraicas - Convocatoria de septiembre de 2004


1. Descripción general de Maude

2/8



• Maude es una herramienta que permite escribir y ejecutar especificaciones

formales axiomáticas. Automatiza el proceso de reducción de expresiones.


• Utiliza un lenguaje de especificación muy parecido al visto en clase. Partes de
la especificación: nombre del módulo y del tipo definido, nombres de los
conjuntos usados, sintaxis de las operaciones y semántica.

• Los TAD se llaman sort y los axiomas equation.

¡Cuidado: la sintaxis es muy estricta!

•

• Página web de Maude:

http://maude.cs.uiuc.edu/

• Utilizaremos la versión 1: http://maude.cs.uiuc.edu/maude1/

• Descarga, instalación y ejecución (versión 1 para Linux):


>> wget http://maude.cs.uiuc.edu/maude1/current/system/maude-linux.tar.Z
>> gunzip -c maude-linux.tar.Z | tar -xvf -
>> cd maude-linux/bin
>> ./maude.linux


• Para salir: quit



Sintaxis
in nombreFich .
red expresión .
quit


•

• Modo de uso.

2. Comandos básicos

Significado
Lee y procesa el archivo con nombre nombreFich.
Reduce una expresión, usando los axiomas definidos para
el tipo.
Salir del programa

¡¡No olvidar terminar las expresiones con " ." (espacio en blanco + punto)!!

editor de textos cualquiera.

o Escribir una especificación formal axiomática en un archivo, usando un
o Ejecutar Maude.
o Cargar el fichero con el comando in.
o Si hay errores, ejecutar quit y corregir la especificación.
o Una vez que la especificación esté bien, probar expresiones usando el
o Salir.
o Las expresiones de ejemplo (para ejecutar con red) también se pueden

comando red.

incluir en otro fichero o en el mismo.

Algoritmos y Estructuras de Datos, 2003/2004
Seminario de Especificaciones Algebraicas - Convocatoria de septiembre de 2004

3/8

3. Formato de especificación

NOMBRE

Natural
CONJUNTOS



N Conjunto de naturales
B Conjunto de booleanos {true, false}

fmod NATURAL is
protecting BOOL .
sort N .


fmod NOMBRE is


protecting NOMBRE .



sort NOMBRE .



SINTAXIS



cero:
→ N
sucesor: N → N
esCero: N → B
igual:
N x N → B
suma: N x N → N

→ Nombre del módulo que se está definiendo.

→ Nombre de los módulos que se importan, es
decir, de los tipos usados en la definición. El
módulo BOOL está definido y contiene el tipo
Bool de los booleanos (true, false, and, or, etc.).

Puede importarse más de un módulo.

→ Nombre del conjunto del TAD que estamos

definiendo en este módulo.

op cero : -> N .
op sucesor : N -> N .
op esCero : N -> Bool .
op igual : N N -> Bool .
op suma : N N -> N .



Respetar la sintaxis:

- Espacios en blanco entre cada una de las partes de la descripción.
- No poner la x del producto vectorial.
- Acabar con: espacio en blanco + punto.

SEMANTICA
∀ m, n ∈ N

1. esCero (cero) = true
2. esCero (sucesor (n)) = false
3. igual (cero, n) = esCero (n)
4. igual (sucesor (n), cero) = false
5. igual (sucesor (n), sucesor (m)) = igual (n, m)
6. suma (cero, n) = n
7. suma (sucesor (m), n) = sucesor (suma (m, n))


vars n, m : N .

eq esCero (cero) = true .
eq esCero (sucesor (n)) = false .
eq igual (cero, n) = esCero (n) .
eq igual (sucesor (n), cero) = false .
eq igual (sucesor (n), sucesor (m)) = igual (n, m) .
eq suma (cero, n) = n .
eq suma (sucesor (m), n) = sucesor (suma (m, n)) .


vars n, m : N . → Nombre de las variables que se van a usar y su tipo.
var b : Bool .
eq exp1 = exp2 . → Axioma (eq → equation).


FIN Natural

endfm

Algoritmos y Estructuras de Datos, 2003/2004
Seminario de Especificaciones Algebraicas - Convocatoria de septiembre de 2004


4/8

• Ejecutar expresiones de ejemplo:


Maude> red suma (sucesor(sucesor (cero)), sucesor (sucesor (cero))) .

Maude> red esCero(suma(sucesor(sucesor(cero)), sucesor(cero))) .



• Para mostrar los axiomas aplicados en cada paso:


Maude> set trace on .

Maude> red esCero(sucesor(sucesor(cero)) .



• Para desactivar la traza:


Maude> set trace off .



ejemplo.maude

• Para guardar los resultados en disco:
o Escribir la especificación y las reducciones en un fichero. Por ejemplo,

o Ejecutar desde la línea de comandos, redirigiendo la salida a un fichero:

o Analizar los resultados en el fichero de salida.


>> ./maude.linux ejemplo.maude > salida.txt

Algoritmos y Estructuras de Datos, 2003/2004
Seminario de Especificaciones Algebraicas - Convocatoria de septiembre de 2004

5/8


fmod NATURAL is
protecting BOOL .
sort N .

op cero : -> N .
op sucesor : N -> N .
op esCero : N -> Bool .
op igual : N N -> Bool .
op suma : N N -> N .

vars n, m : N .

eq esCero (cero) = true .
eq esCero (sucesor (n)) = false .
eq igual (cero, n) = esCero (n) .
eq igual (sucesor (n), cero) = false .
eq igual (sucesor (n), sucesor (m)) = igual (n, m) .
eq suma (cero, n) = n .
eq suma (sucesor (m), n) = sucesor (suma (m, n)) .
endfm



4.2. Fichero: letra.maude

http://dis.um.es/~ginesgm/files/doc/letra.maude



4. Ejemplos

4.1. Fichero: natural.maude

http://dis.um.es/~ginesgm/files/doc/natural.maude



fmod LETRA is
protecting BOOL .
sort L .

op a : -> L .
op e : -> L .
op i : -> L .
op o : -> L .
op u : -> L .
op igual : L L -> Bool .

vars x, y : L .

eq igual (a, a) = true .
eq igual (e, e) = true .
eq igual (i, i) = true .
eq igual (o, o) = true .
eq igual (u, u) = true .
eq igual (x, y) = false .
endfm



Algoritmos y Estructuras de Datos, 2003/2004
Seminario de Especificaciones Algebraicas - Convocatoria de septiembre de 2004

6/8

4.3. Fichero: pila.maude

http://dis.um.es/~ginesgm/files/doc/pila.maude


in letra .

fmod PILA is
protecting BOOL .
protecting LETRA .
sort Mensaje .
sort S .
subsorts Mensaje < L .

op error : -> Mensaje .
op crearPila : -> S .
op esVacia : S -> Bool .
op pop : S -> S .
op tope : S -> L .
op push : L S -> S .

var s : S .
var t : L .

eq esVacia (crearPila) = true .
eq esVacia (push (t, s)) = false .
eq pop (crearPila) = crearPila .
eq pop (push (t, s)) = s .
eq tope (crearPila) = error .
eq tope (push (t, s)) = t .
endfm


4.4. Fichero: ejemplo.maude

http://dis.um.es/~ginesgm/files/doc/ejemplo.maude


in natural .

set trace on .

red suma (sucesor(sucesor (cero)), sucesor (sucesor (cero))) .

set trace off .

red igual(suma(sucesor(cero), cero), sucesor(cero)) .

in pila .

red pop(push(a, push(e, pop (push(i, pop(crearPila)))))) .

red tope(pop(push(a, crearPila))) .

red push (tope(crearPila), crearPila) .

quit



Algoritmos y Estructuras de Datos, 2003/2004
Seminario de Especificaciones Algebraicas - Convocatoria de septiembre de 2004

7/8



prueba1.maude

natural.maude
prueba2.maude



lista.maude
prueba3.maude

arbol.maude
prueba4.maude

Ejercicios

1. (1 punto) Comprobar el resultado de las siguientes expresiones usando las
especificaciones formales definidas en el apartado 4. Decir cuántos axiomas es
necesario aplicar en cada caso:

a) push(tope(push(a, crearPila)), pop(push(e, push(i, crearPila))))
b) igual(sucesor(sucesor(cero)), suma(sucesor(cero), sucesor(cero)))
c) tope(pop(pop(push(i, push(o, push(u, crearPila))))))
d) igual(e, tope(pop(push(e, pop(crearPila)))))

2. (2 puntos) Añadir a la especificación formal del TAD Natural las operaciones:
predecesor, resta, producto, potencia, factorial, esMenor, esMenorIgual,
esPar, mínimo y máximo. Convertir las siguientes expresiones a la notación
definida y comprobar el resultado que se obtiene, indicando el número de
axiomas aplicados.

0) 22*(3-1)
1) (3-2)(2+1)
2) 3+2*2-1!
3) (2*3)(3-1-1)

¿ 3+32 < 3*23 ?
¿ (4+2)*2*1 < 4! ?
¿ mínimo{(2-2)3, 23-3}? ¿ 3! ≤ 1-2-3 ?
¿ Es par (21+1-12) ?
¿ máximo{22!, 22} ? ¿ (2+1)! < (2-3)2+1 ? ¿ Es par (4! - 3!) ?

¿ mínimo{4!, 222} ? ¿ Es par (3! -32) ?
¿ máximo{2(1+2), 2!}? ¿ Es par (2+2 - 2*3) ?

Ojo: no hacer todas las expresiones, sólo las de la fila correspondiente al valor D
calculado con la fórmula: D = (DNI del alumno) módulo 4.

3. (3 puntos) Escribe una especificación formal para el TAD lista de letras. La
especificación debe incluir las operaciones: vacia (devuelve una lista vacía),
insertar (dada una lista y un elemento, inserta el elemento al principio de la
lista), concatenar (unir dos listas), longitud (devuelve la longitud de una lista),
primero, ultimo, cabecera (devuelve todos los elementos menos el último),
cola (devuelve todos los elementos menos el primero), invertir (invierte el
orden de los elementos de una lista), elemento (dada una lista y un entero n,
devuelve el elemento n-ésimo de la lista, siendo el primero el 1, después el 2,
etc.) y buscar (dada una lista y una letra, devuelve un entero que indica la
primera aparición de la letra en la lista). Probar la especificación con al menos 5
expresiones de ejemplo, en las que aparezcan todas las operaciones defi