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:
-
within the same formalism (replacing a module A by a more specific module
B which simulates the behaviour of A);
-
between different formalisms (passing from a more to a less abstract
specification or programming language).
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)