Weakest preconditions, liberal and not (with C.S.Scholten)

Weakest preconditions, liberal and not

by Edsger W.Dykstra and C.S.Schoften

The purpose of this note is to show how for the weakest liberal precondition a predicate transformer wlp can be defined such that

(a) $\left\lbrack {\left( {{w}{p}\left( {S,Q}\right) ∧ {w}{p}\left( {S,T}\right) }\right) = {w}_{p}\left( {S,Q}\right) }\right\rbrack$ for all $Q$ .

Since wlp will be defined recursively over the syntax, the validity of (0) will be proved by induction over the syntax. For the syntax we take the one of the language fragment from "A Discipline of Programming". The reader is supposed to be familiar with EWD813.

By way of preparation we shall prove some simple theorems about predicate transformer pairs (f.g), satisfying

$\left\lbrack {P ⇒ {PQ}}\right\rbrack = \left\lbrack {gP ⇒ Q}\right\rbrack$ for all $P$ and $Q$ .

(Equation (6) of EWD813.) The theorems deal with new solutions of (1) constructed from previous ones; we need them in view of the recursive definitions of wlp.

Lemma 0. Let $\left( {{f}{0},{g}{0}}\right)$ and $\left( {{f}{1},{g}{1}}\right)$ be solutions of (1); then $\left( {{f}{0} \circ {f}{1},{g}{1} \circ {g}{0}}\right)$ is also a solution of (1). (Here "o" is used to denote functional composition.)

Proof. For all $P$ and $Q$ we have

\begin{array}{l} [ P ⇒ (f _ {0} \circ f _ {1}) Q ] \ = {\mathrm {d e f i n i t i o n} o p ^ {\prime \prime} o ^ {\prime \prime} } \ [ P ⇒ p _ {0} (p _ {1} Q) ] \ = {(p _ {0, g 0}) s a t i s f i e s (1) } \ [ g o P ⇒ f _ {1} Q ] \ = {\langle p _ {1}, g _ {1} \rangle \mathrm {s a b i s f i e s} (1) } \ [ g 1 (g 0 P) ⇒ Q ] \ = {\mathrm {d e f i n i t i o n o f} " 0" } \ [ (g 1 \cdot g 0) P ^ {\prime} ⇒ Q ] (\mathrm {E n d o f P r o o f .}) \ \end{array}

Lemma 1. Let $\left( {{p}{i},{g}{i}}\right)$ be solutions of (1) for all $i$ from a set of natural numbers; then $\left( {{p}_{i},g}\right)$ is a solution of

(1) with $f$ and $g$ defined by

[ f Q = (\underline {{A}} _ {i}: {f _ {i} Q }) ] \mathrm {f o r a l l} Q

[ g P = (\underline {{E}} i: g i P) ] f o r a l l P.

Proof. For all $P$ and $Q$ we have

\begin{array}{l} [ P ⇒ f Q ] \ = {\mathrm {d e f i n i t i o n o f} f } \ [ P ⇒ (\underline {{A}} i: f _ {i} Q) ] \ {p r e d i c a t e c a l c u l u s } \ [ (\underset {A} {A} i: \mathcal {P} \rightarrow \mathcal {P} (Q) ] \ = {\text {p r e d i c a t e c a l c u l u s} } \ (A _ {i} \colon [ P ⇒ P _ {i} Q ]) \ = {\overline {{(p _ {i} , g _ {i})}} \mathrm {s a t i s f i e s} (- 1) } \ (\underline {{A}} i: [ g i P ⇒ Q ]) \ = {\text {p r e d i c a t e c a l c u l u s} } \ [ (\underline {{A}} _ {i}: g; P \rightarrow Q) ] \ = {\text {p r e d i c a t e c a l c u l u s} } \ [ (E i: g i P) ⇒ Q ] \ \end{array}

E W D 8 1 6 - 2

= {d e f i n i t i o n o f g }

[ g P ⇒ Q ]

(End of Proof.)

Lemma 2. Let $\left( {p,g}\right)$ satisfy $\left( 1\right)$ ; then $\left( {{pb},{gb}}\right)$ satisfies (1)

with ${fb}$ and ${gb}$ defined by

[ f b Q = (¬ B \lor f Q) ] f o r a l l Q

[ g b P = g (B \wedge P) ] f o r a l l P

where $B$ is an arbitrary predicate.

Proof. For all $P$ and $Q$ we have

[ P ⇒ p b Q ]

= {\mathrm {d e f i n i t i o n o f} p b }

[ P ⇒ (¬ B v f Q) ]

= {\text {p r e d i c a t e c a l c u l u s} }

[ (B ∧ P) ⇒ f Q ]

= {(p, g) s a t i s f i e s (1) }

[ g (\overline {{B}} \wedge P) ⇒ Q ]

= {\mathrm {d e f i n i t i o n o f} g b }

[ g b P ⇒ Q ]

(End of Proof.)

Lemma 3. Let $\left( {{f}{0},g}\right)$ satisfy $\left( 1\right)$ ; then $\left( {{f}{b},g}\right)$ satisfies $\left( 1\right)$ with ${fb}$ and ${gb}$ defined by

[ f b Q = f (B v Q) ] \mathrm {f o r a l l} Q

[ g b P = (¬ B ∧ g P) ] \mathrm {f o r a l l} P

where $B$ is an arbitrary predicate.

EWD816-3

The proof of Lemma 3 is so similar to that of Lemma 2 that it is left to the reader.

We introduce for an arbitrary predicate transformer $f$ the notation $\mathbf{f}^{\mathrm{n}}$ defined by

f ^ {0} \mathrm {i s t h e i d e n t i t y a n d} f ^ {n + 1} = f ^ {0} f ^ {n} \qquad \mathrm {f o r} n ≥ 0.

As a corollary of Lemmata 0,1, and 3 we formulate

Corollary 0. Let $\left( {p,g}\right)$ satisfy (1); then $\left( {{pb},{gb}}\right)$ satisfies

\begin{array}{l} {[ f b Q = (\underline {{A}} i: i \ge 0: f ^ {i} (B \vee Q)) ] \mathrm {f o r a l l} Q} \ {[ g b P = (\underline {{I}} B \wedge (\underline {{E}} i: i \ge 0: g ^ {i} P)) ] \mathrm {f o r a l l} P} \end{array}

where $B$ is an arbitrary predicate.

For the language fragment from "A Discipline of Program- ming" we shall define a weakest liberal precondition wlp. As we go along, we shall show the validity of (o) and, in view of EWD813, that wlp(S,?) is universally conjunctive, so that a strongest postcondition sp(?,S) corresponds to it. For the sake of completeness we repeat their relation

(2) $\left\lbrack {P ⇒ w \mid P\left( {S,Q}\right) }\right\rbrack = \left\lbrack {{sp}\left( {P,S}\right) ⇒ Q}\right\rbrack$ for all $P,Q$ and all $S$ .

abort. [wlp(abort,Q)] for all Q . In view of [7]wp(abort,Q)], for all $Q,(0)$ is satisfied. With the strongest

postcondition defined by [7sp(P,abort)] for all P, (2) is satisfied. By EWD813, Lemma 11, we conclude that wlp(abort,?) is universally conjunctive (and sp(?,abort) is universally disjunctive).

$\therefore {wlp}\left( {{skip},Q}\right) = Q}$ and $\left\lbrack {{sp}\left( {P,{skip}}\right) = P}\right\rbrack$ for all

assignment. Confining ourselves, as in "A Discipline of Pro-gramming" to total expressions $E$ , we define $[wlp("x:=E", Q)=Q_E^x]$ for all $Q$ . From predicate calculus we know that $wlp("x:=E", ?)$ is universally conjunctive, so that $sp(?,"x:=E")$ exists; by EWD813, Lemma 12,

for all $P : \operatorname{sp}\left( {P,{}^{\prime \prime }{}{X = E}}\right)$ is the strongest solution of $\left\lbrack {P ⇒ {X}{E}^{x}}\right\rbrack$ .

In this case we abstain from a more explicit formulation.

concatenation. We define $[wlp("s0; s1", Q) = wlp(S0, wlp(S1, Q))]$ for all $Q$ .

In order to prove that (0) is satisfied, we remark that we have (for all so and S1 and) for all $X$ and $Q$ :

\begin{array}{l} [ X = (w p (^ {n} S _ {0}; S _ {1}, Q) ∧ w p (^ {n} S _ {0}; S _ {1}, T)) ] \ = {\mathrm {d e f i n i t i o n s o f c o n c a t e n a t i o n} } \ [ X = (w) p (S _ {0}, w) p (S _ {1}, Q)) ∧ w p (S _ {0}, w p (S _ {1}, T))) ] \ = {S _ {0} \mathrm {i s a s s u m e d t o s a t h i s p y} (0) } \ [ X = (w l p (S _ {0}, w l p (S _ {1}, Q)) ∧ w l p (S _ {0}, w p (S _ {1}, T)) ∧ w p (S _ {0}, T)) ] \ = {w l p (S o,?) i s a s s u m e d t o b e c o n j u n c t i v e } \ [ X = (w | p (S _ {0}, w | p (S _ {1, Q}) ∧ w p (S _ {1, T})) ∧ w p (S _ {0, T})) ] \ = {S _ {1} \mathrm {i s a s s u m e d t o s a t i s f y (0)} } \ \end{array}

\begin{array}{l} [ X = (w p (S _ {0}, w p (S _ {1}, Q)) ∧ w p (S _ {0}, T)) ] \ = {S O i s a s s u m e d t o s a t i s p y (0) } \ [ X = w p (S _ {0}, w p (S _ {1}, Q)) ] \ = {\mathrm {d e f i n i t i o n o f c o n c a t e n a t i o n} } \ [ X = w p (S _ {0}; S _ {1}, Q) ] \ \end{array}

From the equality of the first and the last line we conclude that (0) is satisfied. From Lemma 0 we conclude that the strongest postcondition defined by

[ s p (P, " S o; S _ {1} ^ {\prime \prime}) = s p (s p (P, S _ {0}), S _ {1}) ]

satisfies (2). Hence $w \mid p\left( {{}^{\prime \prime }{S}{0};{S}{1}^{\prime \prime },\ref{eq:S0}}\right)$ is universally conjunctive.

alternative construct. For the statement IF of the form

IF: $\left{ \begin{array}{ll} {10} & \text{ 若 }{BO} \rightarrow {SO}\left\lbrack \right\rbrack \cdots \left\lbrack \right\rbrack B{n}^{2} \ {n}^{2} & \text{ 若 }{Sn} \rightarrow {BO}\left\lbrack \right. \end{array}\right.$

we define

[ w i p (I F, Q) = (\underline {{A}}: 0. 5 5 \mathrm {s i n}: 7 B i \vee w i p (S i, Q)) ] f o r a l l Q.

In order to prove that (0) is satisfied, we observe for all $X$ , etc. - with, as usual, $[BB = (E_i: 0 ≤ i ≤ n: Bi)]$ - under omission of $C$ 's range

\begin{array}{l} [ X = (w p (1 F, Q) ∧ w p (1 F, T)) ] \ = {\mathrm {d e f i n i t i o n s o f t h e a l t e r n a t i v e c o n s t r u c t s} } \ [ X = ((A _ {i} \because ¬ B _ {i} v w p (S i, Q)) \wedge B B \wedge (\underline {{A}} _ {i} \because ¬ B _ {i} v w p (S i, T))) ] \ = {\text {p r e d i c a t e c a l c u l u s} } \ [ X = (B B \wedge (\underset {i} {\wedge} i: ¬ B i \vee (w l p (S _ {i}, Q) \wedge w p (S _ {i}, T))) ] \ = {\mathrm {t h e} S i \mathrm {a r e a s s u m e d t o s a t i s f y} (0) } \ [ X = (\mathrm {B B} ∧ (\underline {{A}} i: ¬ \mathrm {B} i \lor w p (\mathrm {S} _ {i}, Q))) ] \ = {\mathrm {d e f i n i t i o n o f t h e a l t e r n a t i v e c o n s t r u c t} } \ [ X = w p (1 F, Q) ] \ \end{array}

E W D 8 1 6 - 6

Hence, (0) is satisfied. From Lemmata 1 and 2 it follows that the strongest postcondition satisfying (2) exists and is given by

$\left\lbrack {{sp}\left( {{P}{i} \mid F}\right) = \left( {{E}{i} : {Oset} : {sp}\left( {{B}{i} ∧ {P}{i},{Si}}\right) }\right) }\right\rbrack$ . Hence wlp $\left( {1{F}_{2}?}\right)$ is universally conjunctive.

repetitive construct. For the statement ${DO}$ of the form

DO: $\underset{\partial }{d}0\overset{\partial }{B}0 \rightarrow {S}{0}\left\lbrack \ldots \right\rbrack B{n}^{\prime } \rightarrow {S}{n}\underset{\partial }{d}$

we define, in terms of the corresponding IF,

[ w l p (D O, Q) = (\underline {{A}} i: i \ge 0: k q ^ {i} T) ]

where the predicate transformer ${kg}$ is defined by

[ k q X = (B B v Q) \wedge w l p (l F, X) ] f o r a l l Q a n d X.

Note that, in view of [BB v wlp (IF, X)] for all $X$ , predicate transformer $\mathbf{kg}$ satisfies

[ k q X = (i B B \wedge Q) v (B B \wedge w l p (I F, X)) ] f o r a l l X.

Analogously to the above we rewrite the traditional definition of $\mathbf{w}\mathbf{p}$

[ w p (D O, Q) = (\underline {{E}} i: i \ge 0: h q ^ {i} F) ]

[ w p (D O, T) = (\underline {{E}} c: c ≥ 0: h t ^ {t} F) ]

where the predicate transformers ${hg}$ and ${ht}$ are defined by

E W D 8 1 6 - 7

\begin{array}{l} [ h q X = (¬ B B ∧ Q) \lor w p (I F, X) ] f o r a l l Q a n d X \ [ h + X = 7 B B \vee w _ {P} (1 F, X) ] \qquad \mathrm {f o r a l l} X. \ \end{array}

We derive for all $X, Y,$ and $Z$

[ Z = k q X \wedge h + Y ]

\begin{array}{l} \begin{array}{r l} & {= {\mathrm {d e f i n i t i o n s o f k g a n d h t} }} \ & { [ Z = ((¬ B B ∧ Q) v (B B ∧ w l p (I F, X))) ∧ (¬ B B v w p (J F, Y)) ]} \end{array} \ = {\mathrm {p r e d i c a l e c a l c u l u s} } [ 2 = (¬ B B ∧ Q) \lor (B B ∧ w | _ {P} (I F, X) ∧ w _ {P} (I F, Y)) ] \ \begin{array}{r l} & {= {\mathrm {s i n c e} [ w p (1 F, Y) ⇒ B B ] }} \ & { [ Z = (¬ B B ∧ Q) \lor (w p (1 F, X) ∧ w p (1 F, Y)) ]} \end{array} \ \begin{array}{r l} & {= \left{\left[ w _ {p} (I F, Y) ⇒ w _ {p} (I F, T) \right] \right}} \ & { [ Z = (¬ B B ∧ Q) v (w _ {p} (I F, X) ∧ w _ {p} (I F, T) ∧ w _ {p} (I F, Y)) ]} \end{array} \ \begin{array}{r l} & {= {(0) \mathrm {i s s a t i s f i e d f o r} S = I F }} \ & {[ Z = (¬ B B ∧ Q) \lor (w p (I F, X) ∧ w p (I F, Y)) ]} \end{array} \ = {w p i s c o n j u n c t i v e } [ 2 = (¬ B B ∧ Q) v (w p (I F, X ∧ Y)) ] \ \begin{array}{l} {= {\mathrm {d e f i n i t i o n o f} h g }} \ {[ Z = h g (X ∧ Y) ] , h e n c e} \end{array} \ \end{array}

(3) [ k q X \wedge h + Y = h q (X \wedge Y) ] \mathrm {f o r a l l} X, Y

We can now prove

Lemma 4. For all natural $i$

[ k g ^ {i} X \wedge h t ^ {i} Y = h g ^ {i} (X \wedge Y) ] f o r a l l X, Y.

Proof. The Lemma being correct for $i = 0$ , we proceed with a proof by mathematical induction by observing for all $X, Y,$ and $Z$

\begin{array}{l} [ Z = k g ^ {i + 1} X \wedge h + ^ {i + 1} Y ] \ = \left{ \begin{array}{l l} \mathrm {d e f i n i t i o n o f i t e r a t e d f u n c t i o n a l c o m p o s i t i o n} \ [ 2 = k q (k q ^ {i} X) \wedge h t (h t ^ {i} Y) ] \end{array} \right. \ = {(3) } [ Z = h g (k q ^ {i} X \wedge h t ^ {i} Y) ] \ = {\mathrm {i n d u c t i o n h y p o t h e s i s} } [ 2 = h q (h q ^ {2} (X ∧ Y)) ] \ = {\mathrm {d e f i n i t i o n o f i t e r a t e d f u n c t i o n a l c o m p o s i t i o n} } [ Z = h q ^ {i + 1} (X ∧ Y) ] (\mathrm {E n d o f P r o o f .}) \ \end{array}

Applying Lemma 4 to the case $[X] \wedge [Y]$ we obtain

(4) $\left\lbrack {{kg}^{i}T ∧ h{t}^{i}F = h{g}^{i}F}\right\rbrack$ for all natural i ,

from which we immediately derive

\begin{array}{l} t r u e \ = {(4) } \ [ (\underline {{E}} j: j ≥ 0: (\underline {{A}} i: i ≥ j: k q ^ {i} T \wedge h + ^ {i} F)) = (\underline {{E}} j: j ≥ 0: (\underline {{A}} i: i ≥ j: h q ^ {i} F)) ] \ = {\text {p r e d i c a t e c a l c u l u s} } \ [ (\underline {{E}} j: j \ge 0: (\underline {{A}} i: i \ge j: k g ^ {i} T)) \wedge (\underline {{E}} j: j \ge 0: (\underline {{A}} i: i \ge j: h t ^ {i} F)) = \ (E j: j \ge 0: (\underline {{A}} c: c \ge j: h q ^ {i} F)) ] \ = {\text {s e e b e l o w *}) } \ [ (A i: i ≥ 0: k g ^ {i} T) \wedge (\underline {{E}} i: i ≥ 0: h t ^ {i} F) = (E i: i ≥ 0: h q ^ {i} F) ] \ = {\mathrm {d e f i n i t i o n s} \mathrm {o f} w l p (D O, Q), w _ {P} (D O, T), \mathrm {a n d} w _ {P} (D O, Q) } \ [ w p (D O, Q) \wedge w p (D O, T) = w p (D O, Q) ] \ \end{array}

Hence, (0) is satisfied for $S = {DO}$ .

*) The expression $\left( {{\underline{\operatorname{Ej}}}{i} : j ≥ 0 : \left( {{\underline{\operatorname{A}}}{i} : i ≥ j : {X}{i}}\right) }\right)$ equals a) $\left( {{E}{i} : i ≥ 0;{X}{i}}\right)$ if ( $A : i ≥ 0 : \left\lbrack {{X}{i} ⇒ {X}{i + 1}}\right\rbrack$ ) holds ,in which case we might call the ${X}{i}$ "a weakening sequence",

b) $\left( {\underline{A} : i ≥ 0 : {X}{i}}\right)$ if $\left( {\underline{A} : i ≥ 0 : \left\lbrack {{X}{i + 1} ⇒ {X}{i}}\right\rbrack }\right)$ holds,in which case we might call the ${X}{i}$ "a strengthening sequence".

In view of the monotonicity of the predicate transformer ${kg}$

Remark Had we so desired, we could have defined

\begin{array}{l} [ w l p (D O, Q) = (\underline {{E}} j: j \ge 0: (\underline {{A}} c: i \ge j: k q ^ {i} T)) ] \ [ w p (D O, Q) = (\underline {{E}} j: j \ge 0: (\underline {{A}} c: c \ge j: h q ^ {i} F)) ] \ \end{array}

We leave it to the reader to decide whether he thinks these more symmetric definitions misleading or illuminating. (End of Remark.)

Remains to be shown that the predicate transformer wlp(Do,?) is universally conjunctive. This follows directly from Corollary 0 thanks to the following alternative expression for wlp(Do,Q)

[ w l _ {p} (D O, Q) = (\underline {{A}} i: i \ge 0: w l _ {p} (1 F ^ {i}, B B \vee Q)) ]

This follows from the fact that for all natural $i$

(5) $\left\lbrack {{kq}^{i}T = \left( {\underline{A}j : 0 ≤ j < i : w}\right) p\left( {I{F}^{j},B{B}^{v}Q}\right) }\right\rbrack$

Proof Relation (5) obviously holds for $c = 0$ . We proceed by mathematical induction. We observe for all $Z$

[ Z = k q ^ {i + 1} T ]

\begin{array}{l} = {\mathrm {d e f i n i t i o n o f i t e r a t e d f u n c t i o n a l c o m p o s i t i o n} } \ [ Z = k g (k g ^ {2} T) ] \ = {\mathrm {d e f i n i t i o n o f} k q } \ [ Z = (B B \vee Q) \wedge w l p (I F, k g ^ {i} T) ] \ = {\mathrm {i n d u c t i o n h y p o t h e s i s (5)} } \ [ Z = (B B \vee Q) ^ {j} \wedge w l p (I F, (\underline {{A}} _ {j}: 0. 5 j < i: w l p (I F ^ {j}, B B \vee Q))) ] \ = {w l p (I F, ?) i s c o n j u n c t i v e } \ [ Z = (B B \vee Q) \wedge (\underline {{A}} _ {j}: 1 ≤ j < i + 1: w l p (I F ^ {j}, B B \vee Q)) ] \ = \left{\left[ B B \vee Q = w l _ {p} (I F ^ {0}, B B \vee Q) \right] \right} \ [ Z = (\underset {j} {A}) _ {j: 0 ≤ j < i + 1: w l p (I F ^ {j}, B B \vee Q)}) ] (\mathrm {E n d o f P r o o f .}) \ \end{array}

Finally we conclude from Corollary 0

[ s p (P, D O) = (¬ B B \wedge (\underline {{E}}: c: c ≥ 0: s p (P, I F ^ {c}))) ] f o r a l l P.

Critical remarks, We are not too satisfied with the large number of competing expressions for wlp (D0,Q) that have been used in the above, a baroqueness, which makes this note unfit for publication.

Furthermore, its title is not entirely appropriate; the note deals with strongest postconditions and expressions for them as well. We could have confined ourselves to the definition of wlp ; the proof of (o) would be very much like the above, the proofs of wlp's universal conjunctivity would be given directly, and the existence of a strongest postcondition would, hence, have been settled. The expressions for the strongest postconditions could then have been delegated to an appendix. Though more disentangled, such a text would probably have been longer.

As a piece of positive criticism we note that the subsequent

lines of our proofs are all connected by equality signs, thus giving rise to strong results. The experience is a further incentive to use equality instead of implication wherever possible. (End of Critical Remarks.)

In the past we have experimented with different concepts for the strongest postcondition, viz.

${sp}^{\prime }\left( {p,s}\right)$ is the strongest predicate $X$ satisfying

sp" (P, S) is the strongest predicate X satisfying $\left\lbrack {{P}{\Lambda }{w}{P}\left( {S,T}\right) ⇒ {w}_{P}\left( {S,X}\right) }\right\rbrack$ .

The experiments failed: sp' is not a total function and for sp" concatenation did not correspond to functional composition.

22 April 1982

drs. C.S. Schohen

Scientific Adviser

Philips Research Laboratories

5600 MD EINDHOVEN

The Netherlands

prop. dr. Edsger W. Dgksta

Burraughs Research Fellow

Plataanstraa 5

5671 AL NUENEN

The Netherlands