Parameterized theories and views in full Maude 2.0

Francisco Durán, José Meseguer

Research output: Contribution to journalConference article

Abstract

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.

Original languageEnglish (US)
Pages (from-to)316-338
Number of pages23
JournalElectronic Notes in Theoretical Computer Science
Volume36
DOIs
StatePublished - Dec 1 2000
Externally publishedYes
EventThe 3rd International Workshop on Rewriting Logic and its Applications - Kanzawa, Japan
Duration: Sep 18 2000Sep 20 2000

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Parameterized theories and views in full Maude 2.0'. Together they form a unique fingerprint.

Cite this