Maude
De Wikipedia, la enciclopedia libre
Maude es un lenguaje de programación para especificaciones formales mediante el uso de términos algebraicos. Se trata de un lenguaje interpretado que permite la verificación de propiedades y transformaciones sobre modelos y que permite ejecutar la especificación como si fuera un prototipo.
Maude soporta de una manera sistemática y eficiente la reflexión lógica. Esto permite a Maude ser un lenguaje extremadamente potente y extensible, permitiéndole soportar un álgebra de operaciones de composición de módulos extensible, además permite muchas aplicaciones avanzadas de metaprogramación y metalenguaje. De hecho, algunas de las aplicaciones más interesantes de Maude son aplicaciones de metalenguaje, en las cuales Maude es usado para crear entornos ejecutables para distintas lógicas, demostraciones de teoremas, lenguajes y modelos de computación.
Este lenguaje puede modelar casi todo, cualquier cosa que se pueda escribir, hablar o describir mediante el lenguaje humano, se puede expresar con instrucciones Maude. Puede llegar a ser extremadamente abstracto, su diseño permite tanta flexibilidad que la sintaxis puede parecer más bien abstracta.
Tabla de contenidos |
[editar] Core Maude
Llamamos Core Maude al intérprete de Maude implementado en C++ y que provee toda la funcionalidad básica del lenguaje.
- Sintaxis básica
En Maude los elementos sintácticos básicos son los identificadores, usados para poner nombre a módulos, tipos y operadores. Las unidades básicas de especificación y programación son los módulos. Existen tres tipos de módulos: los módulos funcionales, los módulos de sistema y los orientados a objetos.
Lo primero que una especificación necesita es declarar los tipos (denominados sorts) de los datos definidos y las correspondientes operaciones. Los sorts están parcialmente relacionados mediante relaciones de subtipo (subsort) definiéndose un orden parcial.
La lógica en la que se basa Maude es la lógica ecuacional de pertenencia. En esta lógica los tipos se agrupan en clases de equivalencia llamados kinds. Para este propósito, dos tipos se agrupan en clases de equivalencia llamados kinds. Para este propósito, dos tipos se consideran equivalentes si pertenecen al mismo componente conexo. En Maude los tipos están definidos por el usuario mientras que los “kinds” son implícitamente asociados con componentes conexos de tipos y son consideramos como “supertipos de error”.
Las variables en Maude se declaran restringiéndose a un determinado dominio de un tipo o “kind”. Un término es una constante, una variable, o la aplicación de un operador a una lista de términos argumento. El tipo de una constante o variable es su sort declarado.
- Módulos funcionales
Los módulos funcionales definen tipos de dato y operaciones sobre ellos en forma de teorías ecuacionales. Los tipos de datos consisten en elementos que pueden ser nombrados por términos base. Dos términos denotan el mismo elemento si y sólo si pertenecen a la misma clase de equivalencia; esto viene determinado por las ecuaciones. La semántica de un módulo funcional es su álgebra inicial. En los módulos funcionales, una aplicación repetida de ecuaciones como reglas de simplificación eventualmente alcanza un término al cual no se le pueden aplicar más ecuaciones, y el resultado, llamado forma canónica, es el mismo independientemente del orden en el que se hayan aplicado las reglas. Para reducir un término hasta su forma canónica se usa la instrucción:
red TérminoAReducir .
Un módulo funcional se declara usando las siguientes palabras claves:
fmod <NombreDelMódulo> is
<DeclaracionesYDefiniciones>
endfm
En Maude, la definición de una operación empieza por la palabra reservada op, seguida del nombre de la operación, dos puntos, la lista de tipo de los parámetros separados por espacios en blanco, el símbolo ->, el tipo del resultado y un punto. Todas las operaciones tienen que devolver un valor y sólo uno, pero no es necesario que tenga parámetros. Los operadores constantes se definen como aquellos que no tienen ningún argumento. También permite la sobrecarga de operaciones, es decir, se pueden definir varias operaciones con el mismo nombre, pero con una lista distinta de parámetros.
Además los operadores pueden tener atributos que proveen información adicional sobre el operador: semántica, sintáctica, etc. Se declaran entre [...], después del tipo devuelto y antes del punto de fin de línea. Los más importantes son:
• assoc (asociatividad)
• comm (conmutatividad)
• idem (idempotencia)
• id: <Término> (identidad, con el correspondiente término para el elemento de identidad)
• iter (iterador, permite definir operadores unarios con un carácter de iterador)
• ctor (constructor, a partir de ellos obtenemos todos los valores del tipo)
- Módulos de sistema
Un módulo de sistema en Maude especifica una teoría de reescritura. Una teoría de reescritura tienen tipos, kinds y operadores, y puede tener tres tipos de definiciones: ecuaciones, axiomas de pertenencia y reglas.
Un módulo de sistema se declara usando las siguientes palabras claves:
mod <NombreDelMódulo> is
<DeclaracionesYDefiniciones>
endm
- Importación de módulos
Cada módulo de sistemas o funcional puede importar otros módulos como submódulos. En Maude puede ser importado de tres maneras diferentes: en modo protecting, extending o including.
Protecting: Importar un módulo en modo Protecting significa que no se le añade basura (definir nuevos términos irreducibles a los tipos definidos en el módulo importado) y confusión (agregar reglas de reducción que hacen que términos que eran distintos ahora no lo sean) cuando es importado.
Extending: Permite la adición de basura pero no de confusión.
Including: Permite la adición de basura y/o de confusión.
- Corrección de una especificación
Para que la especificación de una operación sea sintácticamente correcta ha de cumplir tres condiciones: tiene que ser confluente (si hay varias reducciones posibles se ha de llegar siempre al mismo término canónico), completa (todo término básico no canónico se ha de poder reducir), y libre de reducciones infinitas (no deben existir secuencias de reducciones de longitud infinita). La corrección semántica requiere una correspondencia entre el funcionamiento de las operaciones especificadas y las propiedades del álgebra modelo deseada.
- Operaciones generadoras
Las funciones generadoras se marcan con el atributo [ctor]. Un término es canónico si sólo incluye operaciones generadoras. Si todos los términos canónicos representan elementos distintos, el conjunto de generadores es libre. Si el conjunto de generadores no es libre necesitamos ecuaciones impurificadoras, que establecen la equivalencia de términos canónicas.
Especificación de los naturales en Maude
fmod NATURAL is
sort Natural .
*** generadores
op 0 : -> Natural [ctor] .
op suc : Natural -> Natural [ctor iter] .
*** constructores
op _+_ : Natural Natural -> Natural [comm assoc id: 0] .
op _*_ : Natural Natural -> Natural [comm assoc] .
*** variables
vars M N : Natural .
*** ecuaciones
eq suc(M) + suc(N) = suc(suc(M + N)) .
eq 0 * N = 0 .
eq suc(M) * N = (M * N) + N .
endfm
Especificación de los números complejos en Maude
fmod COMPLEJOS is
including INT .
sort complejo .
*** generadores
op <_;_> : Int Int -> Complejo [ctor] .
*** constructores
op _+_ : Complejo Complejo -> Complejo .
op _-_ : Complejo Complejo -> Complejo .
*** variables
vars A B C D : Int .
*** ecuaciones
eq < A ; B > + < C ; D > = < A + B ; C + D > .
eq < A ; B > - < C ; D > = < A - B ; C - D > .
endfm
[editar] Full Maude
Full Maude es una extensión de Maude, escrito en el mismo lenguaje, que dota a Maude de un potente y extensible álgebra de módulo en el cual los módulos de Maude pueden ser combinados conjuntamente para construir módulos más complejos. Los módulos pueden ser parametrizados, y pueden ser instanciados usando los views (vistas). Los parámetros son teorías especificando los requerimientos semánticos para una correcta instanciación. Las teorías mismas pueden ser parametrizadas.
Los módulos de Core Maude también pueden ser introducidos en Full Maude.
- Programación parametrizada
Los bloques básicos de esta programación parametrizada son: módulos parametrizados, teorías y vistas.
Teorías: Se usan para declarar interfaces de módulo, o sea la sintaxis y propiedades semánticas que tienen que ser satisfechas por lo parámetros actuales usados en una instanciación. Se declaran mediante las palabras claves fth…endfth. Todas ellas pueden tener tipos, subtipos, operadores, variables, axiomas de partencia, ecuaciones y pueden importar otras teorías o módulos.
Vistas: Las usamos para especificar como un módulo destinado tiene que satisfacer una teoría fuerte. En general, hay muchas maneras mediante las cuales tales requerimientos pueden ser satisfechos; puede haber diferentes vistas, cada una especificando una interpretación particular de la teoría fuente en el destino. Cada declaración de vista tiene asociado un conjunto de obligaciones, para cada axioma en la teoría fuente tiene que haber un caso en el que la traducción del axioma por la vista es true en el destino. Se declara mediante view…endv
Módulos parametrizados: Es la instanciación de un módulo usando como parámetro una vista sobre una teoría.
Teoría TRIV (predefinida en Maude)
fth TRIV is
sort Elt .
endfth
Vista de los naturales sobre la teoría TRIV
view VNat from TRIV to NAT is
sort Elt to Nat
endv
[editar] Enlaces externos
- Página oficial de Maude
- Proyecto MOMENT, Maude para Windows
- Manual Maude
- Depurador declarativo para Maude
