Module Operations

Abstract

Specifications and code should be structured in modules of relatively small size to facilitate understandability of large systems, increase reusability of components, and localize the effects of system changes. In Maude, these goals are achieved by means of a module algebra that supports parameterized programming techniques in the OBJ3 style [146] as well as the definition of module hierarchies, i.e., acyclic graphs of module importations; that is, each functional or system module can import other Maude modules as submodules. Since the submodule relation is transitive, we can in this way develop module hierarchies. Mathematically, we can think of such hierarchies as partial orders of theory inclusions, that is, the theory of the importing module contains the theories of its submodules as subtheories.

As in Clear [33], OBJ [146], and other specification languages in that tradition, the abstract syntax for writing specifications in Maude can be seen as given by module expressions, where the notion of module expression is understood as an expression that defines a new module out of previously de- fined modules by combining and/or modifying them according to a specific set of operations. In fact, structuring is essential in all specification languages, not only to facilitate the construction of specifications from already existing ones—with more or less flexible reusability mechanisms—but also for managing the complexity of understanding and analyzing large specifications. Maude supports module operations for summation, renaming, and instantiation of parameterized modules.

Section 8.1 introduces module importations and the different modes in which such importations can take place. Section 8.2 discusses the summation and renaming module expressions. Section 8.3 introduces parameterized programming, including the use of theories and views, the parameterization of functional and system modules, and the instantiation of parameterized modules. We refer to [98, 110, 111] for a deeper discussion on the semantics of the Maude module operations.