DISI Dipartimento di Informatica e Scienze dell'Informazione

Implementation of Derived Programs (Almost) for Free

M. Cerioli and E. Zucca .

In F. Parisi Presicce, editors, Recent Trends in Data Type Specification, Lecture Notes in Computer Science, Berlin, 1998. Springer Verlag. To Appear.

In the process of top-down software development, an implementation step can consists of two different kinds of refinement: A property that we usually expect to hold is that these two kinds of refinement can be composed, i.e, if a module A is correctly implemented by B, then all the programs which use A can be correctly transformed in programs which use B, provided that we are able to translate linguistic constructs from the more to the less abstract level.
Our aim is to give a model for this situation independent from the particular formalisms which are involved, in the spirit of the theory of institutions.
To this end, we introduce a notion which is partly similar to that of parchment (syntactic representation of an institution), since we assume that in a given formalism the expressions over a signature can be defined as a free standard many-sorted algebra.
Anyway, we require a much stronger uniformity w.r.t. parchments, since this free algebra is independent from the specific signature. That corresponds to the fact that in many concrete cases the expressions of the formalism can be defined once at all in an inductive way as terms, and any specific signature only gives a family of symbols which can be used as variables in the corresponding terms.
In this case, it is actually possible to factorize an implementation step in a uniform and a specific part, the latter only depending on the particular program.

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