Properties of Simulation
Correctness of an implementation $\equiv$ the corresponding diagrams commute weakly.
Composing Simulation Diagrams
Concatenation of Simulation Diagrams
Note that 3 and 4 doesn’t require any condition to $\alpha$.
Vertical Composition of Simulation Diagrams
Implications between Simulations
If $\alpha$ is total and functional the four simulations are equivalent.
Data Invariants and Totality of Abstraction Relations
Using data invariant can convert partial abstraction relation to total one by restricting data type on reachable subset.
Soundness of Simulation
Soundness of simulation, that is, simulation between data types implies data refinement.
Theorem 4.10 (Soundness of simulation)
L- and L$^{-1}$-simulation are sound. U-simulation is sound if the abstraction relation is total. U$^{-1}$-simulation is sound if the abstraction relation is functional.