Maude

A reflective equational rewrite logic programming language in the OBJ Family of executable specification languages.

Maude programs consist of modules which specify a set of term types, equations that should hold within the module over those types along with some annotations, and declarations that explain what manner of relations (such as importing) the module has with other modules. The equational reductions that Maude specifies are concurrent in that they can be applied in any order.

However, Maude is even more interesting because the rewriting theory that it uses is universal. That is, it can express the reduction strategy of any other logic, including itself. The way this is done is that the default reduction strategy is contained within the strategy meta-module, and there can be further such modules that provide modified forms of it. Maude's (relatively complicated) form of expression quotation allows the possibility of modifying this in small ways without the full overhead of a static meta-module specification. This means that "backtracking" and other procedural hacks in logical languages are avoided in favor of a direct manipulation of the language as needed, so it will most often be totally transparent to the program (which is a specification, so this is important to keep out the "how" elements).


Pages in this topic: MobileMaude   Real-Time Maude   Reflection in Maude   Syntax in Maude  


Also linked from: ADATE   Algebraic Specification   CafeOBJ   José Meseguer   Metalogical Reflection   Methods of Reflection   Rewrite Logic 101   Sprint   Tactic   Trotskyite Tunes