Goal and Motivation

During the process of stepwise, hierarchical program development, a step represents a transformation of a so-called abstract higher level result into a more concrete lower level one. In general, this development process corresponds to increasing the amount of detail required for the eventual implementation of the original specification on a given machine.

In the first part of this book we develop the relational theory of simulation and a general version of Hoare logic, show how data refinement can be expressed within this logic, extend these results to total correctness, and show how all this theory can be uniformly expressed inside the refinement calculus of Ralph Back, Paul Gardiner, Carroll Morgan and Joakim von Wright. We develop this theory as a reference point for comparing various existing data refinement methods in the second part, some of which are syntax-based methods. This is one of the main reasons why we are forced to clearly separate syntax from semantics.

The second part of this monograph focuses on the introduction of, and comparison between, various methods for proving correctness of such transformation steps. Although these methods are illustrated mainly by applying them to correctness proofs of implementations of data types, the techniques developed apply equally well to proving correctness of such steps in general, because all these methods are only variations on one central theme: that of proof by simulation, of which we analyze at least 13 different formulations.