Simulation, our main technique for proving data refinement, also works for proving refinement of total correctness between data types based on the semantic model introduced in the previous chapter. However, certain complications arise; for instance, L−1-simulation is unsound in case abstract operations expose infinite nondeterminism, which severely restricts the use of specification statements.

Section 9.1 extends the soundness and completeness results for simulation from Chapter 4 to total correctness. As the main result, we present in Section 9.2 a total correctness version of our L-simulation theorem from Chapter 7.

Simulation

The semantics-based notions of data type, data refinement, and simulation need not be defined anew. The only notion changed is that of observation since, through our total correctness program semantics, nonterminating behaviors have also become observable. It is essential to the understanding of total correctness simulation between data types to realize that, semantically speaking, abstraction relations are directed. In particular, the relational inverse of an abstraction relation from level C to level A is not an abstraction relation in the opposite direction, as is the case for partial correctness. Now it becomes clear why several authors prefer the name downward simulation for L-simulation and upward simulation for L−1-simulation [HHS87]: the direction of an L-simulation relation is downwards, from the abstract to the concrete level, whence a more descriptive name for it would be representation relation or downward simulation relation. For this reason we redefine the meaning of ⊆Lβ such that β itself (and not its inverse) is used in the inclusions characterizing L-simulation.