The nondeterminacy considered thus far in this monograph was loose in the sense of [Park 1979]: any choice or sequence of choices allowed by the command is acceptable behaviour of the implementation, but the fact that a choice is allowed does not mean that it can ever occur.

While reasoning about concurrent computations, and in the design of communicating processes, we have to deal with unpredictable execution, which is yet not completely loose. We may want to assume that a computation delegated to another process eventually yields an answer or that, if a stream of messages is sent, eventually an acknowledgement comes back.

Such assumptions are called fairness assumptions. Fairness is a subject in itself with a highly operational flavour. There are many different kinds of fairness, cf. [Francez 1986] and [Lehmann e.a. 1981], but it seems that most definitions cannot elegantly be expressed in terms of predicate-transformation semantics. Therefore, we restrict ourselves to predicative fairness, a kind of fairness proposed in [Morris 1990] and [Queille-Sifakis 1983].

In the literature, fairness is usually treated only for repetitions. In [Morris 1990], fairness of tail-recursive procedures without mutual recursion is treated. We give a definition applicable to arbitrary procedures. Our formalization is in agreement with the treatment of loc.cit. in the case of tail recursion. Mutual recursion and ‘calls before the tail’ seem to be adequately treated. Our formalization leads to overly optimistic specifications if a procedure body contains sequentially ordered recursive calls.

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.

In this chapter, we develop syntactic criteria on commands, which imply disjunctivity properties for their weakest preconditions. We suppose that the disjunctivity properties of the simple commands are known and try to generalize these properties to procedures and composite commands. From this chapter onward, the theory of Chapter 4 is indispensable.

In Section 8.1 we introduce, for a given set R of predicate transformers, a set of commands called the syntactic reflection Sy.R of R. The main property is that wp.q ∈ R for all q ∈ Sy.R. In Section 8.2 we provide methods to prove that a command belongs to the syntactic reflection.

In Section 8.3 the theory is specialized to the case that R is characterized by a disjunctivity property. Section 8.4 contains the next specialization, namely to the classes of total commands, of disjunctive commands, and of finitely nondeterminate commands. For our purposes the first two classes merely serve as examples or test cases. Our real aim is the class of the finitely nondeterminate commands. It is this class, or rather its syntactic reflection, that plays a key role in Chapters 11 and 13.

Syntactic reflection of semantic properties

Throughout this section we let R be a sup-closed subset of MT. We are interested in syntactic criteria on commands c ∈ A⊙ that imply wp.c ∈ R. Our solution consists of an algebraic definition of a subset Sy.R of A⊙ with wp.q ∈ R for all q ∈ Sy.R.

In this chapter, we reconcile the definition of the semantics of recursive procedures, cf. Chapter 4, with the relational semantics of Chapter 6. The idea is that the two semantical paradigms meet halfway. Therefore, the chapter consists of two parts.

The first part is based on predicate-transformation semantics, cf. Chapter 4. In Section 9.1, we describe the stack implementation of recursive procedures. This implementation can be regarded as an interpreter: the whole recursive declaration is interpreted by means of a tail-recursive procedure with a stack of continuations as a value parameter. The correctness of the interpreter is proved in Section 9.2.

In the second part of the chapter we treat the relational semantics of recursive procedures. This is done in two steps. In Section 9.3, we define the relational semantics of a tail-recursive declaration by means of a transitive closure in a graph of configurations. By Chapter 6, these relational semantics induce predicate transformers. We then show that the predicate transformers correspond to wp and wlp as defined for such a declaration in Chapter 4. In Section 9.4, the ideas and results of the preceding sections are combined. The stack implementation of 9.1 is combined with the relational semantics of tail recursion (cf. Section 9.3) to define the relational semantics of an arbitrary recursive declaration. The results of 9.2 and 9.3 imply that these relational semantics correspond to the predicate-transformation semantics of Chapter 4.

This chapter is devoted to the introduction of annotations, procedures, recursion and repetitions, all concepts highly relevant to programming practice and programming methodology. In 2.1 we introduce Hoare triples as a specification method. Hoare triples are used in 2.2 for correctness proofs by annotation. In 2.3 and 2.4 we treat procedures in a programming language like Pascal. The specification and invocation rules are discussed in Section 2.3. The correctness of recursive procedures is treated in Section 2.4. The methods presented here are not new but deserve to be promoted.

In Section 2.5 we present and prove an abstract version of the rule for total correctness of recursive procedures. In 2.6 we introduce homomorphisms, functions from commands to predicate transformers that satisfy the standard laws of wp and wlp. Homomorphisms are used in 2.7 to give Hoare's Induction Rule for conditional correctness of recursive procedures, and a related rule for the necessity of preconditions. Finally, in Section 2.8, the results on recursive procedures are specialized to the repetition.

With respect to recursive procedures, this chapter is not ‘well-founded’. We only postulate some properties and proof rules, but the definition of the semantics of recursion (i.e., of the functions wp and wlp) and the proof of the postulates are postponed to Chapter 4.

Specification with Hoare triples

Weakest preconditions provide the easiest way to present predicate–transformation semantics. The formalism of Hoare triples, however, is completely equivalent and more convenient for program derivations and proofs of program correctness.