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.