Prev Up Next
Go backward to 1.2 Core Maude
Go up to 1 Introduction
Go forward to 1.4 Applications

1.3 Full Maude

Using reflection, Core Maude can be extended to a much richer language with an extensible module algebra of module operations that can make Maude modules highly reusable. The basic idea is that META-LEVEL can be extended with new data types--extending its Module sort to richer sorts for structured and parameterized modules--and with new module operations--such as instantiation of parameterized modules by views, flattening of module hierarchies into single modules, desugaring of object-oriented modules into system modules, and so on. In particular, this supports an OBJ style of parameterized programming [27], with highly generic and reusable modules. All such new types and operations can be defined in Core Maude. This, together with the explicit access to modules as terms provided by reflection, makes the corresponding module algebra completely open, and easily extensible by new module operations and transformations.

Using the meta-parsing and meta-pretty printing functions in META-LEVEL and a simple LOOP-MODE module providing input/output, we can in addition develop in Core Maude a suitable user interface for Full Maude. At present, Full Maude supports all of Core Maude plus object-oriented modules, parameterized modules, theories with loose semantics to state formal requirements in parameters, views to bind parameter theories to their instances, and module expressions instantiating and composing parameterized modules.


Prev Up Next