Parameterized theories and views in full Maude 2.0

Parameterized specification and programming is a key modularity and reusability technique crucial for managing the complexity of large specifications and programs. In the search for ever more powerful parameterized module composition operations, languages in the Clear/OBJ tradition, including OBJ3, CafeOBJ, and Maude, have used categorical constructions involving three key notions: (i) modules, which are theories with an initial or, more generally, free extension semantics; (ii) theories, with a loose semantics; and (iii) views, which are theory interpretations used to instantiate parameter theories, and to assert formal properties. It has for long been understood that the full generality and power of a module algebra based on these notions requires parameterized theories and views, not just parameterized modules. However, at present, none of the above-mentioned language implementations supports parameterized modules and views. This paper explains and illustrates with examples the language design of Full Maude 2.0, a new module algebra for Maude currently under development in which modules, theories, and views can all be parameterized. We also summarize the underlying categorical semantics, based on the notion of structured modules with freeness constraints, and explain the reflective design of the Full Maude 2.0 implementation. We are very thankful to Narciso Martí-Oliet for his collaboration in the development of this work, for his careful reading of several versions of the paper, and for his many helpful suggestions for improvement. We are also greatful to Joseph Goguen for his constructive criticism and comments on these ideas.