The following abstract is from [4]. A framework is developed
for studying the implementation process, as a stepwise process in which an
abstract specification is successively transformed to reach a final
compilable specification adapted to the computer environment. In this
context, an implementation relation is referred to as the relation which
should link any 'valid' implementation to its abstract formal specification.
In other words, the implementation relation is intended to express formally
the notion of validity. Our framework allows the exact characterization of
the transformations which may take place at each step for a given
implementation relation. This framework is essential for dealing with
non-transitive implementation relations. In the second part of the paper,
these results are exemplified in on some existing relations, and an
apparent paradox is presented. Some new results about these relations are
also derived.