Su diseño permite tanta flexibilidad que la sintaxis puede parecer en principio poco comprensible.
El sistema Maude ha demostrado imperfecciones en protocolos de criptografía solamente especificando lo que el sistema puede hacer y descubriendo situaciones no deseadas (como estados o términos a los que no debería ser posible llegar).
Los elementos sintácticos básicos son los identificadores, usados para poner nombre a módulos, tipos y operadores.
Lo primero que una especificación necesita es declarar los tipos (denominados sorts) de los datos definidos y las correspondientes operaciones.
Para tal caso, dispondríamos de una estructura como la siguiente: Como podemos observar hemos definido tanto el tipo ListaEntNV como ListaEnt.
En esta lógica los tipos se agrupan en clases de equivalencia llamados kinds.
Para este propósito, dos tipos se consideran equivalentes si pertenecen al mismo componente conexo.
Esto puede verse algo más claro en el siguiente ejemplo: A priori, esta operación no parece que presente ningún problema.
Las variables se declaran restringiéndose a un determinado dominio de un tipo o “kind”.
Los tipos de datos consisten en elementos que pueden ser nombrados por términos base.
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.
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: La propiedad de conmutatividad es en este caso muy útil ya que en muchas ocasiones nos ahorra definir algunas ecuaciones.
Si todos los términos canónicos representan elementos distintos, el conjunto de generadores es libre.