Extreme solutions of equations

Abstract

In the previous chapter we have encountered a number of statements S, for which the predicate transformers wlp(S,?) and wp(S,?) were given in closed form. In the next chapter we shall encounter a statement for which the predicates wlp(S,X) and wp(S,X) are given as solutions of equations of the form

$${\text{Y }}:{\text{ }}\left[ {{\text{b}}.\left( {{\text{X}},{\text{Y}}} \right)} \right].$$

((0))

Here, b is a function from predicate pairs to predicates, i.e. b.(X,Y) is a boolean structure, [b.(X,Y)] is a boolean expression in X and Y , which for given X and Y is either true or false.