El sistema Maude es una implementación de la lógica de reescritura . Es similar en su enfoque general a la implementación OBJ3 de la lógica ecuacional de Joseph Goguen , pero se basa en la reescritura de la lógica en lugar de la lógica ecuacional ordenada por orden, y con un gran énfasis en una poderosa metaprogramación basada en la reflexión .
Maude es un software gratuito y hay tutoriales disponibles en línea. Fue desarrollado originalmente en SRI International , [1] pero ahora lo desarrolla una colaboración diversa de investigadores. [2]
Maude se propone resolver un conjunto de problemas diferente al de los lenguajes imperativos ordinarios como C , Java o Perl . Es una herramienta de razonamiento formal, que puede ayudarnos a verificar que las cosas están “como deberían”, y mostrarnos por qué no están si así es. En otras palabras, Maude nos permite definir formalmente lo que entendemos por algún concepto de una manera muy abstracta (sin preocuparnos de cómo se representa internamente la estructura, etc.), pero podemos describir lo que se considera equivalente en nuestra teoría. ( ecuaciones ) y qué cambios de estado puede atravesar ( reescribir reglas ).
Los módulos de Maude (teorías de reescritura) constan de un lenguaje de términos más conjuntos de ecuaciones y reglas de reescritura. Los términos en una teoría de reescritura se construyen utilizando operadores (funciones que toman 0 o más argumentos de algún tipo , que devuelven un término de un tipo específico). Los operadores que toman 0 argumentos se consideran constantes y se construye su lenguaje de términos mediante estas construcciones simples. Maude permite al usuario especificar si los operadores son infijos, postfijos o prefijos (predeterminado); esto se hace utilizando guiones bajos como rellenos para los términos de entrada.
Se supone que las ecuaciones de reducción son confluentes y terminantes . Las reglas de reescritura no tienen esta restricción.
Cuando Maude "ejecuta", reescribe los términos de acuerdo con las ecuaciones y reescribe las reglas. Maude reescribe los términos de acuerdo con las ecuaciones siempre que hay una coincidencia entre los términos cerrados que uno intenta reescribir (o reducir) y el lado izquierdo de una ecuación en nuestro conjunto de ecuaciones. Una coincidencia en este contexto es una sustitución de las variables en el lado izquierdo de una ecuación que la deja idéntica al término que se intenta reescribir/reducir. Las ecuaciones y las reglas de reescritura también pueden ser reglas condicionales , lo que significa que deben cumplir algunos criterios para ser aplicadas al término (aparte de simplemente coincidir con el lado izquierdo de la regla de reescritura).
Las reglas se aplican de forma "aleatoria" mediante el sistema Maude, lo que significa que no se puede estar seguro de que una regla se aplique antes que otra, y así sucesivamente. Si se puede aplicar una ecuación al término, siempre se aplicará antes de cualquier regla de reescritura. La búsqueda integrada de Maude puede buscar estados no deseados y mostrar que no se puede alcanzar dichos estados. Maude tiene la capacidad de controlar qué aplicaciones de reglas se deben intentar en cada paso utilizando la metaprogramación , debido a la propiedad reflectante o la lógica de reescritura.
Maude se ha utilizado para validar protocolos de seguridad y códigos críticos. El sistema Maude ha demostrado fallas en los protocolos de criptografía simplemente especificando lo que el sistema puede hacer y buscando situaciones no deseadas (estados o términos que no deberían ser posibles de alcanzar). Se puede demostrar que el protocolo contiene errores, no errores de programación sino situaciones. Suceden cosas que son difíciles de predecir simplemente siguiendo el "camino feliz" como lo hacen la mayoría de los desarrolladores.
{{cite book}}: CS1 maint: multiple names: authors list (link)