Maude is a high-performance language and system supporting both equational and rewriting logic computation for a wide range of applications. Maude has been influenced in important ways by OBJ3 [27]. In particular, Maude's equational logic sublanguage essentially contains OBJ3 as a sublanguage. The main differences from OBJ3 at the equational level are a much greater performance, and a richer equational logic, namely, membership equational logic [41], that extends OBJ3's order-sorted equational logic [26].
The key novelty of Maude is that--besides efficiently supporting equational computation and algebraic specification in the OBJ style--it also supports rewriting logic computation. Rewriting logic [37] is a logic of concurrent change that can naturally deal with state and with highly nondeterministic concurrent computations. It has good properties as a flexible and general semantic framework for giving semantics to a wide range of languages and models of concurrency [40]. In particular, it supports very well concurrent object-oriented computation. This is reflected in Maude's design by providing special syntax for object-oriented modules. Since the computational and logical interpretations of rewriting logic are like two sides of the same coin, the same reasons making it a good semantic framework at the computational level make it also a good logical framework at the logical level, that is, a metalogic in which many other logics can be naturally represented and implemented [33, 32]. Consequently, some of the most interesting applications of Maude are metalanguage applications, in which Maude is used to create executable environments for different logics, theorem provers, languages, and models of computation.
The rewriting logic research program, although still very young, has shown good signs of vitality, including two international workshops [20, 28], over a hundred research papers (see the references in [42, 28]), and three language implementation efforts, namely ELAN [29, 3] in France, CafeOBJ [24, 23] in Japan, and Maude. Therefore, Maude should be seen as our contribution to the broader collective effort of building good language implementations for rewriting logic. In this regard, a key distinguishing feature of Maude is its systematic and efficient use of reflection--exploiting the fact that rewriting logic is reflective [15, 10]--a feature that makes Maude remarkably extensible and powerful, and that allows many advanced metaprogramming and metalanguage applications.
The present paper documents Maude 1.0, and explains Maude's basic concepts in a leisurely and mostly informal style, illustrating those concepts with examples. Early language design for Maude appeared in [35, 46, 38]. A first implementation of Maude, supporting reflection, was presented and demonstrated at the First International Workshop on Rewriting Logic in September 1996 [13]. A beta version has been available since March 1998 [9].