PDF de programación - TEMA 1. ESPECIFICACIONES FORMALES ALGEBRAICAS EN MAUDE - Algoritmos y Estructuras de Datos

Algoritmos y Estructuras de Datos I
Grado en Ingeniería Informática, Curso 2º



TEMA 1. ESPECIFICACIONES
FORMALES ALGEBRAICAS

EN MAUDE



Contenidos:



1. Descripción general de Maude
2. Comandos básicos
3. Formato de especificación
4. Ejemplos
5. Actividad de evaluación continua del tema 1



OJO: Antes de realizar esta actividad es conveniente repasar las especificaciones
formales algebraicas o axiomáticas (tema 1 de la asignatura).

Algoritmos y Estructuras de Datos I
Actividad T1. Especificaciones Algebraicas en Maude



2/8



1. Descripción general de Maude

 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. Los tipos

abstractos se definen dentro de módulos (fmod … endfm).

 Partes de la especificación: nombre del módulo y del tipo definido; nombre de

los conjuntos usados; sintaxis de las operaciones; y semántica de las mismas.

 Los TAD se llaman sort y los axiomas equation.

¡Cuidado: la sintaxis es muy estricta! Se diferencian mayúsculas/minúsculas.



 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


2. Comandos básicos

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

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



 Modo de uso.

o Escribir una especificación formal axiomática en un archivo, usando un

editor de textos cualquiera.

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 de ejemplo

usando el comando red. Comprobar que el resultado es el esperado.

o Salir.
o Las expresiones de ejemplo (para ejecutar con red) también se pueden

incluir en otro fichero y ejecutar in con ese fichero para probarlas.

Algoritmos y Estructuras de Datos I
Actividad T1. Especificaciones Algebraicas en Maude



3/8

3. Formato de especificación

Natural

NOMBRE

CONJUNTOS



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

fmod NATURAL is
protecting BOOL .
sort N .



fmod NOMBRE is

 Nombre del módulo que se está definiendo. Un

módulo puede contener varios TAD.


protecting NOMBRE .


sort Nombre .



SINTAXIS



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

 Nombre de los módulos que se importan (los que

contienen los tipos usados en la definición). El
módulo BOOL está predefinido y contiene el tipo
Bool de los booleanos (true, false, and, or, not,
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 cartesiano.
- Acabar con: espacio en blanco + punto.

SEMANTICA
 m, n  N

1. esCero (cero) = true
2. esCero (sucesor (n)) = false
3. esIgual (cero, n) = esCero (n)
4. esIgual (sucesor (n), cero) = false
5. esIgual (sucesor (n), sucesor (m)) =

esIgual (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 esIgual(cero, n) = esCero(n) .
eq esIgual(sucesor(n), cero) = false .
eq esIgual(sucesor(n), sucesor(m)) =

esIgual(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 .  Usar var para una variable y vars cuando sean varias.
eq exp1 = exp2 .  Axioma (eq  equation).


FIN Natural

endfm

Algoritmos y Estructuras de Datos I
Actividad T1. Especificaciones Algebraicas en Maude



4/8



 Ejecutar expresiones de ejemplo:


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

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



 Cuidado con los paréntesis y los puntos. Si se ponen menos paréntesis de los
necesarios, se queda esperando que se cierren, y parece que el programa se ha
quedado colgado. Consejo: usar un editor de texto que empareje los paréntesis.


 Para mostrar los axiomas aplicados en cada paso:


Maude> set trace on .
Maude> red esCero(sucesor(sucesor(cero))) .



 Para desactivar la traza (por defecto está desactivada):


Maude> set trace off .



 Para guardar los resultados en disco:

o Escribir la especificación y las expresiones de ejemplo en un fichero. Por

ejemplo, ejemplo.maude


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

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


o Analizar los resultados en el fichero de salida.


o Consejo 1: en caso de obtener un “wrong answer” o un “runtime error” en el juez
on-line al hacer un envío, pinchar sobre el enlace que aparece para ver la causa del
fallo. El juez mostrará una expresión donde tu especificación produce un resultado
incorrecto.


o Consejo 2: recuerda comprobar los ejemplos de reducciones que aparecen en los
enunciados de los problemas, y otras que puedas considerar convenientes. ¡Pero
recuerda no incluir esas reducciones de ejemplo (red) en el fichero .maude al hacer
los envíos al juez!


o Consejo 3: si sigues sin encontrar la causa del error, busca en el Mooshak las
preguntas que otros usuarios han hecho sobre el mismo problema. Puede que alguna
te sea de utilidad. Si no encuentras nada, escribe una nueva pregunta (pero, por
favor, solo después de haber seguido los consejos anteriores y de haberte calentado
un poco la cabeza). Los jueces humanos te contestarán en cuanto puedan. Recuerda
que las preguntas son públicas para todos los usuarios de Mooshak. Si la pregunta es
particular, pregunta a tu profesor en persona.



Algoritmos y Estructuras de Datos I
Actividad T1. Especificaciones Algebraicas en Maude



5/8



4. Ejemplos

4.1. Fichero: natural.maude

*********** NOMBRE ***********
fmod NATURAL is

*********** CONJUNTOS ********
protecting BOOL .
sort N .
sort NoN .
subsort NoN < N .

*********** SINTAXIS *********
op cero : -> N .
op sucesor : N -> N .
op suma : N N -> N .
op esCero : N -> Bool .
op esIgual : N N -> Bool .
op esDistinto : N N -> Bool .

op NODEFINIDO : -> NoN .
op INFINITO : -> NoN .
op NEGATIVO : -> NoN .

*********** SEMANTICA ********
var n m : N .

eq suma(cero, n) = n .
eq suma(sucesor(m), n) = sucesor(suma(m, n)) .
eq esCero(cero) = true .
eq esCero(sucesor(n)) = false .
eq esIgual(cero, n) = esCero(n) .
eq esIgual(sucesor(n), cero) = false .
eq esIgual(sucesor(n), sucesor(m)) = esIgual(n, m) .
eq esDistinto(n, m) = not esIgual(n, m) .
endfm


 Para poner un comentario en Maude, se deben poner tres o más asteriscos

seguidos (***). El comentario se extiende hasta el final de la línea.



4.2. Fichero: vocal.maude


*********** NOMBRE ***********
fmod VOCAL is

*********** CONJUNTOS ********
protecting BOOL .
sort V .

*********** SINTAXIS *********
ops A E I O U : -> V .
op esIgual : V V -> Bool .
op esDistinta : V V -> Bool .

*********** SEMANTICA ********
var v w : V .

eq esIgual(v, v) = true .
eq esIgual(v, w) = false .
eq esDistinta(v, w) = not esIgual(v, w) .
endfm


 Con “ops” se pueden juntar varias operaciones que tengan la misma sintaxis.

Algoritmos y Estructuras de Datos I
Actividad T1. Especificaciones Algebraicas en Maude



6/8


 Ojo: en Maude no hay ambigüedad en los axiomas anteriores. En caso de que se
puedan aplicar varios axiomas distintos para una misma expresión, se aplicará
siempre el que aparezca en primer lugar.



4.3. Fichero: pila.maude


*********** NOMBRE ***********
fmod VOCAL is
*********** CONJUNTOS ********
protecting BOOL .
sort V .
*********** SINTAXIS *********
ops A E I O U : -> V .
op esIgual : V V -> Bool .
op esDistinta : V V -> Bool .
*********** SEMANTICA ********
var v w : V .
eq esIgual(v, v) = true .
eq esIgual(v, w) = false .
eq esDistinta(v, w) = not esIgual(v, w) .
endfm

*********** NOMBRE ***********
fmod PILA is
*********** CONJUNTOS ********
protecting BOOL .
protecting VOCAL .
sort MensajePilas .
sort P .
subsorts MensajePilas < V .
*********** SINTAXIS *********
op pilaVacia : -> P .
op esVacia : P -> Bool .
op push : V P -> P .
op pop : P -> P .
op tope : P -> V .
op ERRORPILAVACIA : -> MensajePilas .
*********** SEMANTICA ********
var p : P .
var v : V .
eq esVacia(pilaVacia) = true .
eq esVacia(push(v, p)) = false .
eq pop(pilaVacia) = pilaVacia .
eq pop(push(v, p)) = p .
eq tope(pilaVacia) = ERRORPILAVACIA .
eq tope(push(v, p)) = v .
endfm


 Para definir mensajes de