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:
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)