This document describes the executable formal specification of Full Maude---a version of Maude supporting a rich module algebra with module hierarchies, parameterization, views, theories, module expressions, and object-oriented modules---which is in fact its implementation in the Maude 1.00 system. We have realized the design of Full Maude, which is described in detail the in Maude system manual and in [Duran99], using the reflective capabilities of the rewriting logic language Maude itself.
The specification of Full Maude in the Core Maude sublanguage deals not only with module operations, but also with the functionality of a complete language, including parsing, pretty-printing, and an execution environment for such a language. The fact that Full Maude has Core Maude as a ``sublanguage'' simplifies somewhat the representation map between them. Nevertheless, the exact same methodology can be used for representing and executing in Maude many other languages and logics.
We emphasize the extensibility of the module algebra with which Maude has been endowed in this way. We present the specification of Full Maude in sufficient detail so that the different extensions of Full Maude become easily understandable. Note that by `extensions' we not only mean those adding new module transformation operations in the style of the transformation from object-oriented modules to system modules, but also new module combining and/or manipulating operations. We illustrate some of the possibilities for extensions of this kind with several examples.
Maude is available free of charge in its web site at maude.cs.uiuc.edu. The complete specification of Full Maude is available as part of the distribution package.
(BibTeX entry) (gzip'ed Postscript)