Bibliographical Notes

The principle of substitutivity is so intuitive that it has often been proposed under various other names. It is called ``semantic implementation correctness" in [60], attributing the term to Gardiner and Morgan [94]. Nipkow [165] gives a similar intuitive definition of ``implementation".

For other references to early work on refinement we refer to the monograph by de Roever and Engelhardt [60].

Typically, Z textbooks do cover operation refinement separately from data refinement, as we do here. However, the other forms of simple refinement are not normally covered independently, although it must have been clear within the Z community that they were possible [196]. Some textbooks even require the abstract and concrete state to be always different in data refinement, to avoid name capture.