Categorical techniques have allowed since then the study of specification-building operations with independence of any specific formalism by different authors, giving rise to a large body of research.

Algebraic specification is now a mature field of Computer Science because of its mathematical foundations. After Clear, the theory of algebraic specification has been implemented in many computing systems, such as OBJ, ACT ONE, ASL, ASF, PLUSS, LPG, Larch, CASL, etc., and has become an important technique in software engineering methodologies.

The language OBJ embodies many of the categorical module composition operations of Clear and has played a major r\^ole in the development of algebraic specification, and, more generally, of declarative programming. OBJ has been extended in different ways, namely towards object-oriented programming in FOOPS, theorem proving in 2OBJ, and logic programming in Eqlog. Other languages that have appeared more recently, like Maude and CafeOBJ, can also be included in the OBJ family of languages.

In all of these languages, the module operations are a central issue. Module
operations belong to the *metalevel* of the logic in question, that is,
they can be seen as functions taking modules and returning other modules as
results. This is in fact the idea behind the module expressions in OBJ3, in
the module algebra by Bergstra, Heering, and Klint, and in subsequent
research. However, in these approaches the user has a fixed repertoire of
operations available, and cannot express them, extend them, or reason about
them *within the logic*. This means that although module operations, and
in particular parameterization, provide certain ``higher-order'' capabilities,
such capabilities remain limited in their applicability and provide only a
fixed repertoire of higher-order operations.

This situation can be changed quite dramatically by introducing the notion of
a *reflective logic*. Informally, a reflective logic is a logic in which
important aspects of its metatheory can be represented at the object level in
a consistent way, so that the object-level representation correctly simulates
the relevant metatheoretic aspects. In other words, a reflective logic is a
logic that can be faithfully interpreted in itself, giving access to its
metatheory. In particular, rewriting logic is reflective.

A reflective logic like rewriting logic opens up many completely new
possibilities for module composition. In a reflective logic, module
operations are definable within the logic itself, providing
higher-order capabilities by defining operations that transform,
combine, and/or manipulate modules. Based on these ideas, it is
possible to extend the *module algebra* of the system, and it is
also possible to create within the logic a formal environment for it
with tools for formal analysis, transformation, and theorem
proving. Moreover, since the module operations are defined in the
logic, this opens up the possibility of meta-reasoning about such
operations within the logic. Furthermore, if the logic is efficiently
executable then the formal specification of module composition
operations can itself be used as a reasonable implementation.

If, in addition, the reflective logic has good properties as a logical
framework, then a logic L
can be represented in such a framework logic F by giving
any *representation map* of the form

Maude is a reflective language based on rewriting logic that essentially contains the OBJ3 language as an equational sublanguage. Rewriting logic extends equational logic and has very good properties as a logical framework, in which many other logics and many semantic formalisms can be naturally represented. Maude's language design and implementation make systematic use of the fact that rewriting logic is reflective, making the metatheory of rewriting logic accessible to the user in a clear and principled way.

Before defining a generic module algebra of very wide applicability we need to define logic-independent notions of module operations. As already mentioned, there is already a large body of work in this direction, originating in the work on Clear and institutions, and realized in languages such as those in the Clear/OBJ tradition.

We are particularly interested in a module algebra framework in which theories
with *loose* semantics and modules with *initial* semantics coexist,
giving rise to a uniform setting. We like to view a module or theory as a more
general form of a structured theory, possibly with initiality
constraints
on parts of its structure. In this setting, we want to be able to support
parameterized theories and also parameterized views, allowing in this way the
structuring of these entities as well. This will improve, not only the
flexibility of the module algebra in the definition of theories and views, but
also the reusability of the different components. Reusability of views is
something to which not much attention has been paid so far. We think that view
reusability can be greatly increased by applying to them the same ideas
developed for theories. We are therefore interested not only in the
definition of parameterized or structured views, but in views going from
structured theories to structured theories.

Traditionally, the semantics of module operations is given in terms of
*flattened* modules, assuming that each module operation results in an
equivalent flat module. We are interested in a more general notion of module
operation. We propose a module algebra of module operations taking structured
theories as arguments and giving structured theories as results. Some initial
results in this direction are given in Chapter 2, introducing the
notion of structured theories in a categorical way and giving some useful
results for them.

As a first step towards a generic module algebra in a framework logic such as rewriting logic, we have defined an extensible module algebra for rewriting logic itself, and have realized that design using the reflective capabilities of the rewriting logic language Maude. We describe in Chapter 3 the language design of Full Maude, which extends Maude with object-oriented notation, and with a number of module operations, namely module hierarchies, module renaming, parameterization of modules, and transformation of object-oriented modules into system modules.

As we shall see in the description of Full Maude, we are not dealing only with a set of module operations. We are dealing with a complete language, including an execution environment for such a language. The fact that Full Maude has Core Maude as a ``sublanguage'' may simplify the representation map between them, but the methodology can be used for many other languages and logics. Once we have an appropriate representation map, we can then define an execution environment for any other logic or language in the same way.

We explain in Chapter 4 the executable formal specification of Full Maude, which is in fact its implementation in the Maude 1.00 system. We do not give the full specification. Instead, we focus on the more interesting parts but still allowing the reader the possibility of understanding the overall picture. For example, we explain in some detail how the transformation from object-oriented modules to system modules, which was originally proposed by Meseguer, is integrated with the overall module algebra; we explain also in some detail the renaming of modules, and the instantiation of parameterized modules.

We should 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:

- a module expression for union of modules, that is, the classical sum or union + operation taking two modules and returning the result of uniting them;
- as a simple, but interesting, example showing the new possibilities for defining module expressions, we present a module expression TUPLE(N) such that, given a nonzero natural number N, it generates a parameterized functional module specifying a tuple of the corresponding size.

But there are many more possibilities. For example, one important area for
defining new module operations is viewing *formal tools* as appropriate
module operations that analyze and transform specifications. We present in
Chapter 5 a substantial example of this kind, namely, a Church-Rosser
checker that analyzes order-sorted equational specifications and generates a
collection of proof obligations that must be satisfied to guarantee the
Church-Rosser property.

(BibTeX entry) (gzip'ed Postscript)

back home Formal Methods and Declarative Languages Laboratory Computer Science Laboratory, SRI International