5 - Notation and Semantics

Summary

In the previous chapter, our proof techniques for data refinement, namely the notions of simulation introduced in Def. 2.1, have been proven adequate in Theorem 4.17 and sound in Theorem 4.10. This establishes proving simulation as an appropriate technique for verifying data refinement.

In Chapters 9 and 10 we shall encounter other notions of data refinement and simulation defined for frameworks different from that of the binary relations considered until now, for which similar soundness and completeness results will be proven.

In Part II of this monograph a number of established methods for proving data refinement will be similarly analyzed. (These methods are: VDM, Z, and those of Reynolds, Hehner, Back, Abadi and Lamport, and Lynch.) This is done by showing to what extent they are special cases of, or are equivalent to, the previously investigated notions of simulation referred to above, which are the subject of Part I of this monograph.

This justifies considering simulation as a generic term for all these techniques, where the connection with data refinement is made through appropriate soundness and completeness theorems.

Now an immediate consequence of our goal of comparing these simulation methods for proving data refinement is that we must be able to compare semantically expressed methods such as L-simulation and the methods of Abadi and Lamport and of Lynch (see Chapter 14) with syntactically formulated ones such as VDM, Z, and Reynolds' method. This implies immediately that we have to distinguish between syntax and semantics. We bridge this gap by introducing interpretation functions for several classes of expressions, such as arithmetic expressions and predicates built on them (see Section 5.2), programs (see Section 5.3), and relations (see Section 5.4).