We come back to the informal description of wp and wlp given in Section 1.2. This description is used to justify two more postulates concerning wp and wlp, the so-called healthiness laws. These postulates are due to [Dijkstra 1976]). They are theorems of the standard relational semantics, but in predicate-transformation semantics they need not be imposed. In fact, recently, some investigators (cf. [Backvon Wright 1989b], [Morgan-Gardiner 1990]) have proposed specification constructs that lead to violations of the laws (so these constructs cannot be expressed in relational semantics). Command serve from the second example in 1.2 belongs to this category.

In the remainder of this book the healthiness laws are imposed since they form the natural boundary of the theory of Chapter 4. Another reason for imposing them is that they hold for all practical imperative languages and for the relational model of computation (see Chapter 6).

In this chapter, we introduce the laws with an informal justification and we treat the main formal implications.

Conjunctivity properties of predicate transformers

Since the healthiness laws prescribe certain properties of the predicate transformers wp.c and wlp.c for commands c, it is useful to introduce these properties for arbitrary predicate transformers.