ISSN 0934-5043, ©British Computer Society 1990

The purpose of this research is to reduce the number of formal proofs
required in * model refinement*, which hinder software development.
It is shown to be applicable to the transformation of models written in
META-IV (the specification language of VDM ) towards their refinement into,
for example, PASCAL or relational DBMSs. The approach includes the
automatic synthesis of retrieve functions between models,
and data-type invariants.

The underlying algebraic semantics is the so-called
* final* semantics ``à la Wand'':
a specification ``is'' a * model* (heterogeneous algebra)
which is the final object (up to isomorphism) in the category of all its
implementations.

The transformational * calculus* approached in this paper follows
from exploring the properties of finite, recursively defined sets.

*
This work extends the well-known strategy of program transformation
to model transformation, adding to previous work on a
transformational style for operation-decomposition in META-IV.
The model- calculus is also useful for improving
model-oriented specifications.
*