4 - Properties of Simulation

Summary

In Chapter 2 it was already mentioned that correctness of an implementation essentially means that the corresponding diagrams commute weakly. Recall that there are four possible ways in which this can be defined, each implying a notion of simulation. This is depicted in Figures 4.1–4.4 for a single operation (note the direction of the inner arrows).

In this chapter the subtle differences between these notions of simulation are studied. Such differences must be taken into account, e.g., when concatenating simulation diagrams. Also we investigate how these notions behave under vertical stacking and how they are related to each other. The outcome has serious consequences for the value of U- and U⁻¹-simulation.

With the necessary technical machinery at hand, we are finally able to show how data invariants can be used to convert partial abstraction relations into total ones.

Then we analyze soundness and completeness of simulation as a method for proving data refinement.

We undertake most of our investigations in a purely semantic set-up, suppressing the distinction between syntax and semantics as much as possible.

Figure 4.1 represents U-simulation, and Figure 4.2 represents L-simulation. The diagrams in Figures 4.3 and 4.4 represent U⁻¹ -simulation and L⁻¹-simulation, respectively. Because a concrete operation can be less nondeterministic than the corresponding abstract operation, we say that the diagrams commute weakly. This weak form of commutativity is expressed by “⊆” in the following definitions. (Strong commutativity would be expressed by “=”.)

Composing Simulation Diagrams

To obtain a compositional theory of simulation, it would be interesting to have a sufficiently strong condition under which these kinds of simulation hold for composed diagrams.