Ingrid M. Rewitzky 1998, 12pp.
Simulation rules provide a simple, sound and complete technique for proving that one data type refines another. This paper expresses the dependence of the soundness and completeness on the programming language by showing how sound and complete simulation rules for a given language are derived from those for its sublanguages. The dependence of the completeness on the semantic model is expressed using a Jonsson/Tarski duality translation between the relational and predicate transformer semantics of data types and simulation rules. Both these dependencies are considered in the context of a simple language for terminating programs.