This chapter is devoted to the formal definition of the semantics of sequential composition, unbounded choice and recursion and to the proofs of the properties of commands that were introduced and used in the previous chapters. The semantics of the simple commands is taken for granted, but otherwise the reader should not rely on old knowledge but only use facts that have already been justified in the new setting. At the end of the chapter, the foundations of the previous chapters will be complete.

Some examples of the theory are given in the exercises at the end of the chapter. The text of the chapter has almost no examples. One reason is that the chapters 1, 2 and 3 may be regarded as examples of the theory. On the other hand, every nontrivial example tends to constitute additional theory.

In Section 4.1, we introduce complete lattices and investigate the lattice of the predicate transformers and some important subsets. Section 4.2 contains our version of the theorem of Knaster–Tarski. A syntactic formalism for commands with unbounded choice is introduced in Section 4.3.

Section 4.4 contains the main definition. From the definition on simple commands, the functions wp and wlp are extended to procedure names and command expressions. In Sections 4.5 and 4.6, the healthiness laws, which are postulated for simple commands, are extended to procedure names and command expressions.