About predicate transformers in general (with C.S.Scholten)

About predicate transformers in general

by Edsger W. Dykstra and C.S. Scholten

Considerations about the relation between "weakest liberal preconditions" and "strongest postconditions" lead to some very general theory about predicate transformers.

In the following $P$ and $Q$ will stand for total predicates defined on a possibly infinite state space; the predicate $T$ is defined to be true in all states, and the predicate $F$ is defined to be false in all states. Universal quantification of a predicate over all states will be denoted by surrounding that predicate by square brackets. This convention allows us to use the logical connectives $(\neg ,\land ,\lor ,\Rightarrow , = ,\neq)$ to construct predicates from predicates, e.g. $P = Q$ is a predicate -true in those and only those states in which $P$ and $Q$ have equal values-, whereas $[P = Q]$ is a boolean -true if and only if in each state $P$ and $Q$ have equal values-.

Furthermore, $f$ and $g$ will stand for predicate transformers, i.e. total functions from predicates to predicates. Application of a predicate transformer will be denoted by juxtaposition, e.g. $PP$ is functional application has the highest priority.

Let $f$ and $g$ be two predicate transformers such that

(0) $\left\lbrack {{P}^{v}{f}^{Q}}\right\rbrack = \left\lbrack {Q{v}^{g}P}\right\rbrack$ for all $P$ and $Q$ .

Such predicate transformers exist, e.g both equal to the identity transformation, or $\left\lbrack {fQ = T}\right\rbrack$ and $\left\lbrack {gP = T}\right\rbrack$ for all $P$ and $Q$ . Note that equation (0) is symmetric in $f$ and $g$ .

Lemma 0. Equation (0) defines a pairing for (some) predicate transformers, i.e. for any $f$ equation (0) admits of at most 1 solution $g$ .

Proof. Let the pairs $\left( {f,{go}}\right)$ and $\left( {f,{g1}}\right)$ both satisfy equation (0), i.e.

$$ [ P v f Q ] = [ Q v g o P ] \quad \mathrm {f o r a l l} P \mathrm {a n d} Q $$

$$ [ P v f Q ] = [ Q v g 1 P ] \quad \mathrm {f o r a l l} P \mathrm {a n d} Q $$

Hence

$$ [ Q \vee g ^ {0} P ] = [ Q \vee g ^ {1} P ] \mathrm {f o r a l l} P \mathrm {a n d} Q $$

On account of lemma 1 we conclude $[g_0P = g_1P]$ for all $P$ . (End of Proof.)

$$ \begin{array}{l} \mathrm {L e m m a 1 . T r o m} [ Q \vee P _ {0} ] = [ Q \vee P _ {1} ] \mathrm {f o r a l l} Q, P _ {0} \mathrm {-} \ \mathrm {l o w s} [ P _ {0} = P _ {1} ]. \end{array} $$

Proof. Substitution of $\neg {P}{0}$ for $Q$ yields $\left\lbrack {\neg {P}{0}v{P}{1}}\right\rbrack$ ; substitution of $\neg {P}{1}$ for $Q$ yields $\left\lbrack {\neg {P}{1}v{P}{0}}\right\rbrack$ . Hence $\left\lbrack {{P}{0} = {P}{1}}\right\rbrack .\left( \text{End of Proof.}\right)$

Before proceeding we introduce some terminology. A predicate transformer $f$ satisfying

(1) $\left\lbrack {f\left( {\underline{A}Q;Q \in S;Q}\right) = \left( {\underline{A}Q;Q \in S;fQ}\right) }\right\rbrack$

for all finite and non-empty sets $s$ of predicates is called "conjunctive". Note that, in order to prove that $f$ is conjunctive, it suffices to prove that $f$ satisfies

$$ [ f (Q _ {0} \wedge Q _ {1}) = (f Q _ {0} \wedge f Q _ {1}) ] \quad \mathrm {f o r a l l} Q _ {0}, Q _ {1}. $$

A predicate transformer $f$ satisfying, (1) for all sets S is called "universally conjunctive, which is therefore a stronger property than just conjunctive. Note that for a universally conjunctive the property [fT] holds.

Lemma 2. A conjunctive predicate transformer $f$ is monotonic, i.e., satisfies

$$ [ P \vee Q ] \Rightarrow [ \neg f (\neg P) \vee f Q ] \quad \mathrm {f o r a l l} P \mathrm {a n d} Q . $$

(A more usual formulation of monotonicity is

$$ [ P \Rightarrow Q ] \Rightarrow [ f P \Rightarrow f Q ] \mathrm {f o r a l l} P \mathrm {a n d} Q. $$

Proof [PVQ]

$$ \begin{array}{l} = {\text {p r e d i c a t e c a l c u l a s} } \ [ (\neg P \land Q) = \neg P ] \ \Rightarrow {f i s a f u n c t i o n } \ \end{array} $$

$$ \begin{array}{l} [ f (\neg P \land Q) = f (\neg P) ] \ = {{i s c o n j u n c t i v e } \ [ (f (\neg P) \land f Q) = f (\neg P) ] \ = {\text {p r e d i c a t e c a l c u l u s} } \ [ \neg f (\neg P) v f Q ] \ \end{array} $$

(End of Proof.)

In the formulation of lemma 0 we said "some" and "at most"; these were no idle precautions, as the next lemma shows.

Lemma 3 Predicate transformers that satisfy (0) are universally conjunctive.

Proof. Let $(p, g)$ satisfy (0); for reasons of symmetry it suffices to show that $f$ is universally conjunctive. For all $P$ and all $S$ we have

$$ \begin{array}{l} [ P \vee f (\neg Q: Q \in S: Q) ] \ = {\mathrm {o n a c c o u n t o f} (0) } \ [ (\underline {{A}} Q: Q \in S: Q) v _ {g} P ] \ = {\text {p r e d i c a t e c a l c u l u s} } \ [ (\underline {{\underline {{A}}}} Q: Q \in S: Q \vee g P) ] \ = {\text {p r e d i c a t e c a l c u l u s} } \ (\underline {{A}} Q: Q \in S: [ Q, v g P ]) \ = {\mathrm {o n a c c o u n t o f} (0) } \ (\underline {{A}} Q: Q \in S: [ P, f Q ]) \ = {\text {p r e d i c a t e c a l c u l u s} } \ [ (\underset {A} {A Q}: Q \in S: P v f Q) ] \ \end{array} $$

$$ E W D 8 1 3 - 4 $$

$$ \begin{array}{l} = {\text {p r e d i c a t e c a l c u l u s} } \ [ P \vee (\underline {{A}} Q: Q \in S: f Q) ] \ \end{array} $$

The first and last lines being equal for all $P$ and all $S$ , application of Lemma 1 completes the proof. (End of Proof.)

The next Lemma can be viewed as the inverse of the previous one.

Lemma 4: For universally conjunctive $f$ the pair $\left( {p,g}\right)$ satisfies (0) with $g$ defined by

for all $P : \;$ $\left\lbrack {gP = \left( {\underline{E}X : \left\lbrack {{Pv}fX}\right\rbrack : vX}\right) }\right\rbrack$

$$ \begin{array}{l} \mathrm {P r o o f .} [ Q \vee g P ] \ = {\mathrm {b e c a u s e} [ ([ P _ {v} f Q ] \land \neg Q) \Rightarrow g P ] } \ [ Q v _ {g} P v ([ P v f Q ] \land \neg Q) ] \ = {\text {p r e d i c a t e c a l c u l u s} } \ [ Q \vee g P \vee [ P \vee f Q ] ] \ = {\text {p r e d i c a t e c a l c u l u s} } \ [ Q v g P ] v [ P v f Q ], h e n c e \ \end{array} $$

(2) $\left\lbrack {{P}_{v}fQ}\right\rbrack \Rightarrow \left\lbrack {{Qv}gP}\right\rbrack$ for all $P$ and $Q$ .

$$ \begin{array}{l} [ Q \vee g P ] \ \Rightarrow {\mathrm {o n a c c o u n t o f L e m m a 2} } \ [ f Q \vee \neg f (\neg g P) ] \ = {\mathrm {d e f i n i t i o n} g a n d \mathrm {d e M o r g a n} } \ \end{array} $$

$$ \begin{array}{l} [ f Q \lor \neg f (\underline {{A}} X: [ P \lor f X ]: X) ] \ = {f \mathrm {i s u n i v e r s a l l y c o n j u n c t i v e a n d d e M o r g a n} } \ [ f Q \vee (E X: [ P \vee f X ]: \neg f X) ] \ \Rightarrow {\text {p r e d i c a t e c a l c u l u s} } \ [ f Q \lor (E X: [ P \lor F X ]: \neg f X \land \neg P) \lor P ] \ = {\mathrm {p r e d i c a t e c a l c u l u s , d e M o r g a n i n p a r t i c u l a r} } \ [ p q v p ] \quad , h e n c e \ \end{array} $$

$$ (3) [ Q \vee g P ] \Rightarrow [ P \vee f Q ] \quad \mathrm {f o r a l l} P \mathrm {a n d} Q. $$

From (2) and (3) follows that the pair $\left( {p,g}\right)$ satisfies(0). (End of Proof.)

Besides the above we derive directly

Lemma 5. For a pair $\left( {p,g}\right)$ satisfying (0),we have

for all $P : g{P}_{1}$ is the weakest solution of $\left\lbrack {{Pv}{f}^{\prime }\left( {1X}\right) }\right\rbrack$ ,

i.e.: (i) $\left\lbrack {{P}{v}f\left( {{G}{I}P}\right) }\right\rbrack$ (ii) $\left\lbrack {{P}_{v}{f}^{\prime }\left( {7Q}\right) }\right\rbrack \Rightarrow \left\lbrack {Q \Rightarrow g{P}^{\prime }}\right\rbrack$ for all $Q$ .

Proof (i) Substitution of $\neg {gP}$ for $\varnothing$ in(0) yields (ii) Substituting $\mathrm{QA}$ for $\mathrm{Q}$ in (0)suffices

on account of $\left\lbrack {\left( {Q \Rightarrow gP}\right) = \left( {{7Q}{v}_{g}P}\right) }\right\rbrack$

(End of Proof.)

Combining the last two lemmata we conclude that for universally conjunctive $f$ the equation $[P \vee P X]$ in

X has a strongest solution.

For predicate transformer f its "conjugate" $f^{*}$ is defined by

$$ [ f ^ {*} P = \neg f (\neg P) ] \quad f o r a l l P $$

Obviously, the conjugate of ${f}^{ * }$ is $f$ .

A predicate transformer $f$ satisfying

(4) $\left\lbrack {f\left( {{EQ} : Q \in S : Q}\right) = \left( {{EQ} : Q \in S : PQ}\right) }\right\rbrack$

for all finite and non-empty sets $s$ of predicates is called "disjunctive". Note that, in order to prove that $f$ is disjunctive, it suffices to prove that $f$ satisfies

$$ [ f (Q _ {0} \vee Q _ {1}) = (f Q _ {0} \vee f Q _ {1}) ] \mathrm {f o r a l l} Q _ {0}, Q _ {1}. $$

A predicate transformer $f$ satisfying (4) for all sets $S$ is called "universally disjunctive", which is therefore a stronger property than just disjunctive. Note that for a universally disjunctive $f$ the property $[fF = F]$ holds.

We observe for any predicate transformer $f$ and any set $S$ of predicates

$$ [ f (\underset {\sim} {A} Q; Q \in S; Q) = (\underset {\sim} {A} Q; Q \in S; f Q) ] $$

$$ \begin{array}{l} = {\mathrm {d e f i n i t i o n o f} f ^ {} \mathrm {a n d d e M o r g a n} } \ [ \neg f ^ {} (\underline {{E}} Q: Q \in S: \neg Q) = (\underline {{A}} Q: Q \in S: \neg f ^ {} (\neg Q)) ] \ = {\mathrm {n e g a h o n o f b o t h s i d e s a n d d e M o r g a n} } \ [ f ^ {} (\underline {{E}} Q; Q \in S; \neg Q) = (\underline {{E}} Q; Q \in S; f ^ {} (\neg Q)) ] \ = {\mathrm {i n t r o d u c i n g} S ^ {} \mathrm {d e f i n e d b y} (\underline {{A}} X:: (\neg X) \in S ^ {} = X \in S) } \ [ f ^ {} (\underline {{E}} Q: Q \in S ^ {}: Q) = (\underline {{E}} Q: Q \in S ^ {}: f ^ {*} Q) ] \ \end{array} $$

where $S$ and $S^$ are of equal cardinality. From the equality of the first and the last line in the above and the equal cardinalities of $S$ and $S^$ we conclude

Lemma 6. For any predicate transformer $f$ we have

$\left( {f\text{is}\operatorname{conjunctive}}\right) = \left( {{f}^{ * }\text{is}\operatorname{disjunctive}}\right)$

Lemma 7. For any predicate transformer $f$ we have

$\left( {f\text{is universally confluent}}\right) = \left( {{f}^{ * }\text{is universally disjunctive}}\right) .$

Expressing in (0)

$$ [ P v \neg f ^ {} (1 Q) ] = [ Q v \neg g ^ {} (1 P) ] \quad \mathrm {f o r a l l} P \mathrm {a n d} Q $$

or, replacing $P$ and $Q$ by their negations and applying

$$ [ (P \wedge P ^ {} Q) = F ] = [ (Q \wedge g ^ {} P) = F ] \mathrm {p o r a l l} P \mathrm {a n d} Q. $$

EWD813-8

Consider now a pair of predicate transformers $(p, g)$ satisfying

(5) $\left\lbrack {\left( {{P}{\Lambda }{fQ}}\right) = F}\right\rbrack = \left\lbrack {\left( {{Q}{\Lambda }gP}\right) = F}\right\rbrack$ for all $P$ and $Q$

We derive from the above and lemma 3

Lemma 8. Predicate transformers that satisfy (5) are universally disjunctive.

We derive from the above and Lemma 4

bemag. For universally disjunctive $f$ the pair $\left( {{p}_{,}g}\right)$ satisfies (5) with $g$ defined by

for all $P : \left\lbrack {{g}^{P} = { A \times \left\lbrack {\left( {P \land PX}\right) = F}\right\rbrack : \neg X}\right) }\right\rbrack$ .

We derive from the above and Lemma 5

Lemma 10. For a pair $\left( {{p}{,}g}\right)$ satisfying (5),we have for all $P : \;g{P}{1}$ is the strongest solution of

$$ [ (P \land f (\neg X)) = F ] $$

$\left( {P \land P\left( {IgP}\right) }\right) = F$

(ii) $\left\lbrack {\left( {P \land P\left( { \neg Q}\right) }\right) = F}\right\rbrack \Rightarrow \left\lbrack {g - p \Rightarrow q}\right\rbrack$ for all $Q$ .

Note. Expression $\left\lbrack {\left( {{P}{1} + F}\right) Q = F}\right\rbrack$ can also be written as $\left\lbrack {7\left( {{P}{1} + F}\right) Q}\right\rbrack .\;\left( {{End} \circ P}\right)$ Note.

Expressing, finally, in (0) only $g$ in terms of its conjugate, we are similarly led to the equation

(6) $\left\lbrack {P \Rightarrow fQ}\right\rbrack = \left\lbrack {gP \Rightarrow Q}\right\rbrack$ for all $P$ and $Q$ .

Note that, in contrast to (0) and (5), equation (6) is not symmetric in $f$ and $g$ . We summarize the results in Lemma 11.12, and 13 :

Lemma 11. Of any pair $(f,g)$ of predicate transformers satisfying (6), $f$ is universally conjunctive and $g$ is universally disjunctive.

Lemma 12. For universally conjunctive $p$ ,the pair $\left( {p,g}\right)$ satisfies (6) with $g$ defined by

for all $P : \;$ [ $gP = \left( {\underline{A}X : \left\lbrack {P \Rightarrow fX}\right\rbrack : X}\right) \rbrack$ ;

for all $P : gP$ is the strongest solution of $\left\lbrack {P \Rightarrow {P}^{x}}\right\rbrack$ .

Lemma 13. For universally disjunctive $g$ ,the pair $\left( {p,g}\right)$ satisfies (6) with $f$ defined by

for all $Q : \left\lbrack {{f}^{Q} = \left( {\underline{\mathrm{E}}X : \left\lbrack {gX \Rightarrow Q}\right\rbrack : X}\right) }\right\rbrack$ ;

for all $Q$ : if $Q$ is the weakest solution of $\left\lbrack {gX \Rightarrow Q}\right\rbrack$ .

Now it is time to tie in with our introductory remark, which referred to weakest liberal preconditions and strongest postconditions.

Let "wlp(S,Q)" denote the weakest condition on the initial state such that firing S is guaranteed not to establish ¬Q (i.e. S establishes Q or fails to terminate). Note that wlp(S,?) is a total predicate transformer and that [wlp(S,T)] holds for all statements S.

Let $sp(P,S)$ denote the strongest assertion guaranteed to be valid upon completion when S has been fired in an initial state satisfying P. Note that sp(?,S) is a total predicate transformer and that [?sp(F,S)] holds for all statements S.

With the above definitions

$$ [ P \Rightarrow w | p (S, Q) ] = [ s p (P, S) \Rightarrow Q ] \quad f o r a l l P, Q $$

is sweetly reasonable: the truth of the left-hand side is the assertion that the firing of S in an initial state satisfying P will either establish Q or lead to nontermination, the truth of the right-hand side is the assertion that the firing of S in an initial state satisfying P will ,upon completion,establish Q .

The above relation, however, is of form (6). As a result we conclude from Lemma 11 that $w|p(S, ?)$ is

universally conjunctive and sp $(?,S)$ is universally disjunctive. From Lemma 12 we conclude

for all $P$ : ${sp}\left( {P,S}\right)$ is the strongest solution of $\left\lbrack {P \Rightarrow w{1}_{P}\left( {S,X}\right) }\right\rbrack$ .

From Lemma 13 we conclude

for all $Q$ : $w|p\left( {S,Q}\right)$ is the weakest solution of $\left\lbrack {{sp}\left( {X,S}\right) \Rightarrow Q}\right\rbrack$ .

Reservation. Our uninhibited quantification "for all $P$ and $Q$ " is a reason for some concern. (End of Reservation.)

17 March 1982

drs. C.S. Scholten

Philips Research Laboratories

5600 MD EINDHOVEN

the Netherlands

profi. dr. Edsger W. Dgkstra

Burroughs Research Fellow

Plataanstraat 5

5671 AL NUENEN

the Netherlands