In this chapter we present a number of more or less isolated extensions of the fundamental concepts. They broaden the view but have no high priority. We do not need the theory of Chapter 4.

In Section 5.1 we give our version of refinement of commands. Refinement is a very important concept in programming methodology. In this book it plays a less prominent rôle. It occurs in some exercises and it comes again to the fore in Chapter 12. Section 5.2 contains an example where a refinement between procedures is proved by means of the induction rules of Section 2.7.

In Section 5.3 we introduce the calculational method of insertion of guards. This method can be regarded as an alternative to annotation. It is especially useful for proofs of semantic equality. In Section 5.4 this method is used to handle a complicated example that is needed in Chapter 12.

Section 5.5 contains a discussion of strongest postconditions.

In Section 5.6 we prepare the ground for an extension of the termination argument used in Theorem 2(16). The harvest is reaped in Section 5.7, where we present a generalization of Theorem 2(16) and a Necessity Rule for wlp.

Refinement and relative refinement

The function of a compiler is to transform programs written in some high-level programming language, say Pascal, into machine instructions.