DISI Dipartimento di Informatica e Scienze dell'Informazione

Algebraic oriented Institutions

M. Cerioli and G. Reggio .
In T. Rus M. Nivat, C. Rattray and G. Scollo, editors, Algebraic Methodology and Software Technology (AMAST'93), Workshops in Computing, pages 103--210. Springer Verlag, 1994.
In many recent applications of the algebraic paradigm to formal specification methodologies, basic frameworks are endowed with new features, tailored for special purposes, that mostly are ``orthogonal'' to the underlying algebraic framework, in the sense that they are instances of a parametric constructions. This lack of generality is conflicting with the ability of changing the basic formalism, and hence with the reuse of methodologies, seen as high-level theoretical tools for the software development.
In any real application two steps can be distinguished in the process of getting the most suitable algebraic formalism: the choice of the most appropriate basic algebraic formalism (i.e. sufficiently powerful for the problem, but non-overcomplex) and the addition of the features needed in the particular case (e.g. entities for structured parallelism or higher-order functions for functional programming). Thus here we propose a modular construction of algebraic frameworks, formalized by means of operations on institutions, used as a synonym for logical formalism, in order to build richer institutions by adding one feature at a time.
Many constructions used in the practice have meaning only for those institutions that represent ``algebraic formalisms''. In order to give sound foundations for the treatment of such operations, a preliminary step is the formal definition of which institutions correspond to algebraic frameworks. Here we propose a first attempt at the definition of algebraic-oriented institutions, that includes all interesting cases. Then, using this definition, we formally define some operations adding features to basic algebraic frameworks and show that the result of such operations applied to any algebraic-oriented institution is an algebraic-oriented institution, too; so that the result can be used as input for other operations, modularly building a formalism as rich as needed by the application.
Technically algebraic-oriented institutions are described by (standard) algebraic specifications, so that both theoretical and software tools are at hand to help in the building process; moreover algebraic specification users already have the know-how to understand and manipulate metaoperations building algebraic formalisms.

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /person/CerioliM/AMAST93.ps.z (43873 Kb).