The operational interpretation of extreme solutions (with C.S. Scholten)

The operational interpretation of extreme solutions

Edsger W.Dgkstra and C.S.Schohen.

For the repetitive construct ${DO} : \underline{do}B \rightarrow S\underline{o}d$ ,

X: [ X \equiv (B \vee R) \wedge (B \vee w _ {P} (S, X)) ]

and $w$ lp $\left( {{DO},{R}_{1}}\right)$ as the weakest solution of

X: [ X \equiv (B \vee R) \wedge (¬ B \vee w l p (S, X)) ] ,

the two equations being related by

[ w p (S, X) \equiv w p (S, t r u e) ∧ w | p (S, X) ]

From an operational point of view we know that an activation of the repetition leads to one of four mutually exclusive courses of events (with respect to some postcondition $R$ )

the repetition terminates in a final state satis- lying R

the repetition terminates in a final state satis

the repetition "continues", i.e. leads to an infinite sequence of activations of $s$

-- the repetition "gets stuck", i.e. leads to a non-terminating activation of $s$

The purpose of this note is to characterize for each of these four courses of events the initial

condition under which it may occur. As a by-product we shall obtain an operational justification of the above definitions of $w p\left( {{DO},R}\right)$ and $w {l}_{P}\left( {{DO},R}\right)$ .

We begin by observing that the postulated dichotomy of final states into those satisfying R and those satisfying $\pi \mathbb{R}$ presupposes the existence of what we call "point predicates".

In the sequel $p,q,$ and $r$ are variables of type "point predicate". Their properties are captured by the axioms

[ Q \equiv (\underline {{E}} _ {P}: [ P ⇒ Q ]; p) ] \mathrm {f o r a n y} Q \tag {0}

[ p ⇒ ¬ Q ] \equiv ¬ [ p ⇒ Q ] f o r a n y p, Q

By substituting true for $Q$ ,we obtain

$\left\lbrack {\left( {E}_{P} : P\right) }\right\rbrack$ (2)

from (1) $¬ \left\lbrack {¬ p}\right\rbrack$ for any $p$ (3)

Lemma 0 For any bag $V$ of predicates and any point predicate $p$ we have

[ p ⇒ (\underline {{E}} X: X _ {\mathrm {i n}} V: X) ] = (\underline {{E}} X: X _ {\mathrm {i n}} V: [ p ⇒ X ])

\begin{array}{l} \mathrm {P r o o f} \ ¬ [ p ⇒ (\underline {{E}} X: X _ {\mathrm {i n}} V: X) ] \ = {(1) a n d d e M o r g a n } \ [ p ⇒ (¬ X:: ¬ X) ] \ = {\text {p r e d . c a l c .} } \ \end{array}

\begin{array}{l} (A X: [ p ⇒ 7 X ]) \ = {(1) a n d d e M o r g a n } \ ¬ (\underline {{E}} X: X _ {\mathrm {i n}} V: [ p ⇒ X ]) \ \end{array}

(End of Proof.)

Lemma 1 For any bag $V$ of point predicates we have

[ (\underline {{E}} p: p \underline {{i n}} V: p) \equiv (\underline {{A}} q: \tau (q \underline {{i n}} V): \tau q) ]

\mathrm {P r o o f}

t r u e

= {(2) a n d p r e d. c a l c }

[ (\underline {{E}} q: \tau (q \underline {{i n}} V): q) \vee (\underline {{E}} p: p \underline {{i n}} V: p) ]

= {\mathrm {p r e d . c a l c . a n d d e M o r g a n} }

[ (\underline {{A}} q: ¬ (q \underline {{i n}} V): ¬ q) ⇒ (\underline {{E}} p: p \underline {{i n}} V: p) ]

f r u e

= {\text {p r e d . c a l c .} }

(\exists p, q: p \underline {{i n}} V ∧ ¬ (q \underline {{i n}} V): ¬ [ p \equiv q ])

= {\mathrm {p r e d . c a l c .} }

(\underset {\sim} {A} p, q: p \in V ∧ ¬ (q \in V): ¬ [ p ⇒ q ] \lor ¬ [ q ⇒ p ])

= {(1) }

(\underline {{A}} _ {p, q}: p \underline {{i n}} V \wedge ¬ (q \underline {{i n}} V): [ p ⇒ ¬ q ] \vee [ q ⇒ ¬ p ])

= {\text {p r e d . c a l c .}; \text {n o t e t h a t} [ Q ⇒ ¬ P ] \equiv [ P ⇒ ¬ Q ] }

\begin{array}{l} [ (\underline {{E}} _ {p}: p \mathrm {i n} V: p) ⇒ (\underline {{A}} _ {q}: q (q \mathrm {i n} V): q) ] \ (E n d o f P r o o f.) \ \end{array}

So much for the point predicates.

*

In order to show our heuristics we start by in- vestigating under what circumstances a single execution

of $S$ ,started in state $p$ ,may lead to state $q$ . By virtue of the standard operational interpretation

[ p ⇒ w l p (S, 7 9) ] \equiv " n o e x e c u t i o n o f S, s t a r t e d i n p, l e a d s t o q".

Negating both sides, we find

7 [ p ⇒ w | p (S, 1 9) ] \equiv " t h e r e e x i s t s a n e x e c u l i o n o f S , s t a r t e d i n p , t h a t l e a d s t o q".

On account of (1) and the definition of the conjugate, the left-hand side can be rewritten as

[ p ⇒ w | p ^ {*} (S, q) ]

So much for the relation between $p$ and $q$ for

[ p ⇒ B ] \equiv " i n s t a t e p, S i s s t a t e d a n o t h e r t i m e".

Combining those two, we get

[ p ⇒ B ∧ w l p ^ {*} (S, q) ] \equiv " i n \underline {{d o}} B \rightarrow S \underline {{o d}}, s t a t e q i s a p o s s i b l e s u c c e s s o r o f s t a t e p".

With $f$ defined by $\left\lbrack {fX \equiv {\pi }^{1}B \vee \omega \mid p\left( {S,X}\right) }\right\rbrack$ ,the left-hand side is $\left\lbrack {p ⇒ {p}^{ * }q}\right\rbrack$ . Note that this $f$ is universally conjunctive.

So much for our heuristics. Our next section explores in abstracto the relation $\left\lbrack {p ⇒ {f}^{ * }q}\right\rbrack$ for universally conjunctive $f$ .

With respect to predicate transformer $f$ the relation $\frac{su}{c}$ (for "successor") between point predicates is defined by

q \underline {{\operatorname {s u c}}} p \equiv [ p ⇒ p ^ {*} q ] \mathrm {f o r a l l} p, q.

Relation des (for "descendant") is defined as the reflexive transitive closure of suc, i.e. the strongest transitive relation satisfying

p \underline {{\mathrm {d e s}}} p \mathrm {f o r a l l} p

9 \underline {{\mathrm {s u c}}} p ⇒ 9 \underline {{\mathrm {d e s}}} p \mathrm {f o r a l l} p, q

(We have refrained from denoting $\underline{\text{des by}}$ ${\underline{\operatorname{Suc}}}^{ * }$ because the star is already used to denote the conjugate.)

A "descending chain on $p$ " is a sequence of point predicates $q\left( {0 ≤ i}\right)$ satisfying

[ 9 0 \equiv p ] \qquad a n d

(\underline {{A}} i: q (i + 1) \underline {{s u c}} q i)

Note that descending chains may be of finite length; in the last formula the range of $i$ is understood to be such as to encompass all elements of the chain.

We now turn our attention to the equation

X: [ X \equiv Y ∧ f X ] \tag {4}

with universally conjunctive $f$ . (Parameter Y has been introduced for the sake of brevity: our

results will only be used with a few very specific choices for $Y$ .)

In the following, $gY$ is defined as the strongest solution of (4) and $hY$ as its weakest. We re-call from EWD84ga-4-

$g$ is unboundedly conjunctive; h is universally conjunctive;

[ g (Y \wedge Z) \equiv g ^ {\prime} Y \wedge h Z ] \mathrm {f o r a l l} Y, Z. (5)

Our relevant results are captured by the following two theorems:

Theorem 0. For any point predicate $p$

$\left\lbrack {p ⇒ g\text{true}}\right\rbrack \equiv \forall$ all descending chains on $p$ are finite

Theorem 1. For any point predicate $p$ and any predicate

[ p ⇒ h Y ] \equiv (\underline {{A}} q: q \underline {{\mathrm {d e s}}} p: [ q ⇒ Y ])

Proof of Theorem 0 The proof is by showing that in

$7\left\lbrack {p ⇒ g\text{true}}\right\rbrack \equiv$ "there exists an infinite descending chain on $p$ "

each side implies the other.

\begin{array}{l} L ⇒ R \ ¬ [ p ⇒ g \mathrm {t r u e} ] \ = {(1) } \ [ p ⇒ ¬ g t r u e ] \ = {g \mathrm {t r u e i s a s o l u t i o n o f} (4) \mathrm {w i t h t r u e f o r Y 3} \ [ \tilde {p} ⇒ ¬ f (g \text {t r u e}) ] \ = {\mathrm {d e f i n i t i o n o f c o n j u g a t e} } \ [ p ⇒ f ^ {} (7 g t r u e) ] \ = {(0) } \ [ p ⇒ f ^ {} (E q: [ q ⇒ ¬ g ⇒ ¬ g ]; q) ] \ = {f ^ {x} i s u n v e r s a l l y d i s j u n c t i v e } \ [ p ⇒ (\exists q: [ q ⇒ ¬ g ⇒ ¬ q ]: f ^ {} q) ] \ = {L e m m a 0 } \ (E q: [ q ⇒ ¬ g ⇒ e ]: [ p ⇒ f ^ {} q ]) \ = {(1), d e f i n i t i o n o f s u c a n d p r e d. c a l c. } \ (E q: q \sup p: 7 [ q ⇒ g \mathrm {t r u e} ]) \ \end{array}

We conclude that any point predicate solving the equation $x: (x ⇒ g ⇒ 1)$ has a successor solving that equation, from which the existence of the infinite descending chain follows.

$R ⇒ L$ Let $q \in \left( {i ≥ 0}\right)$ be an infinite descending chain on $p$ .

\begin{array}{l} t r u e \ = {\mathrm {d e f i n i t i o n s o f} q _ {i} \mathrm {a n d o f} \underline {{s u c}} } \ (\underline {{A}} i: 0 ≤ i: [ q i ⇒ p ^ {*} (q (i + 1)) ]) \ = {\mathrm {p r e d . c a l c . a n d d e f i n i t i o n o f c o n j u g a t e} } \ (\underline {{\underline {{A}}}} _ {i}: 0 \le i: [ p (¬ q (i + 1)) ⇒ ¬ q _ {i} ]) \ ⇒ {\mathrm {p r e d . c a l c .} } \ \end{array}

\begin{array}{l} [ (\underline {{A}} _ {i}: 0 ≤ i: f (7 q (i + 1))) ⇒ (\underline {{A}} _ {i}: 0 ≤ i: 7 q _ {i}) ] \ ⇒ {\mathrm {s t r e n g t h e n i n g t h e a n t e c e d e n t b y} ^ {\prime} P (1 9 0) \wedge^ {\prime \prime} } \ [ (\underline {{A}} i: 0 ≤ i: f (¬ q _ {i})) ⇒ (\underline {{A}} i: 0 ≤ i: ¬ q _ {i}) ] \ = {f _ {i} \mathrm {i s u n v e r s a l l y c o n j u n c t i v e} } \ [ f (\underline {{A}} i: ¬ q _ {i}) ⇒ (\underline {{A}} i: ¬ q _ {i}) ] \ ⇒ {g \mathrm {t r u e i s t h e s t r o n g e s t s o l u t i o n o f (4) w i t h} \ t r u e P o r Y; K n a s t e r T a r s k i \ [ g \mathrm {t r u e} ⇒ (\underline {{A}} i: ¬ q i) ] \ ⇒ {\mathrm {w e a k e n i n g t h e c o n s e q u e n t} \mathrm {a n d} [ q 0 \equiv p ] } \ [ g \mathrm {t r u e} ⇒ p ] \ = {\mathrm {p r e d i c a t e c a l c u l u s} } \ [ p ⇒ g \mathrm {t r u e} ] \ = {(1) } \ ¬ [ p ⇒ g ⇒ r u e ] \ \end{array}

(End of Proof of Theorem 0.)

\mathrm {P r o o f o f T h e o r e m 1}

\begin{array}{l} \begin{array}{l} L ⇒ R \ \dots \dots \dots \end{array} \mathrm {I n v i e w o f t h e d e f i n i t i o n o f d e s i t s u p p i c e s} \ [ p ⇒ h Y ] ⇒ [ p ⇒ Y ] \qquad a n d \ [ p ⇒ h Y ] ⇒ (\underline {{A}} q: q \underline {{s u c}} p: [ q ⇒ h Y ]) \ \end{array}

\begin{array}{r l} & {\mathrm {S i n c e h Y i s a s o l u t i o n o f (4) , w e h a v e [ h Y ⇒ Y ] ,}} \ & {\mathrm {f r o m w h i c h t h e f i r s t o n e f o l l o w s . F o r t h e s e c o n d o m e ,}} \ & {\mathrm {l e t q b e a s u c c e s s o r o f p . W e o b s e r v e}} \end{array}

\begin{array}{l} [ p ⇒ h Y ] ∧ ¬ [ q ⇒ h Y ] \ = {(1) } \ [ p ⇒ h Y ] ∧ [ q ⇒ ¬ h Y ] \ ⇒ {h Y i s a s o l u t i o n o f (4), h e n c e [ h Y ⇒ f (h Y) ] } \ \end{array}

\begin{array}{l} [ p ⇒ f (h Y) ] ∧ [ q ⇒ h Y ] \ ⇒ {[ p ⇒ p ^ {} q ] a n d p ^ {} i s m o n o t o n i c } \ [ p ⇒ f (h Y) ] ∧ [ p ⇒ f ^ {*} (T h Y) ] \ = {\mathrm {d e f i n i t i o n o f c o m j u g a t e a n d p r e d i c a t e c a l c u l u s} } \ [ - p ] \ = {(3) } \ f a l s e. \ \end{array}

H e n c e [ p ⇒ h Y ] ⇒ [ q ⇒ h Y ].

\begin{array}{l} R ⇒ L. T o b e g i n w i t h w e d e f i n e p r e d i c a t e P b y \ [ P \equiv (\underline {{E}} q: q \underline {{d e s p}}: q) ] (6) \ \end{array}

\mathrm {o r} [ P \equiv (\underline {{A}} _ {9}: 7 (9 \underline {{d e s}} p): 7 9) ] , (7)

\begin{array}{l} (6) a n d (7) b e i n g e q u i v a l e n t o n a c c o u n t o f L e m m a 1. \ S i n c e p \mathrm {d e s} p w e c o n c l u d e f r o m (6) \ [ p ⇒ P ] (8) \ \end{array}

\begin{array}{l} \begin{array}{l} {\mathrm {W e s h a l l f i r s t p r o v e a b o u t} P \mathrm {t h a t} [ P ⇒ F P ].} \ {\mathrm {T o t h i s e n d w e o b s e r v e}} \end{array} \ t r u e \ = {\mathrm {t r a n s i t i v i t y a n d d e f i n i t i o n o f} \underline {{\mathrm {d e s}}} } \ (\underline {{A}} q, r: \underline {{r}} \underline {{s u c}} q \wedge q \underline {{d e s}} p: r \underline {{d e s}} p) \ = {\mathrm {p r e d . c a l c .} } \ (\underline {{A}} q, r: q \underline {{\mathrm {d e s}}} p \wedge ¬ (r \underline {{\mathrm {d e s}}} p): ¬ (r \underline {{\mathrm {s u c}}} q)) \ = {d e f i n i t i o n o f \underline {{s u c}} } \ (¬ q, r: q \underline {{\mathrm {d e s}}} p \wedge ¬ (r \underline {{\mathrm {d e s}}} p): ¬ [ q ⇒ f ^ {*} r ]) \ = {(1) a n d d e f i n i t i o n o f c o n j u g a t e } \ (\underline {{A}} q, r: q \underline {{\mathrm {d e s}}} p \wedge ¬ (r \underline {{\mathrm {d e s}}} p): [ q ⇒ f (¬ r) ]) \ \end{array}

\begin{array}{l} = {\mathrm {p r e d . c a l c .} } \ [ (\underline {{E}} q: q \underline {{\mathrm {d e s}}} p: q) ⇒ (\underline {{A}} r: ¬ (r \underline {{\mathrm {d e s}}} p): f (¬ r)) ] \ = {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} } \ [ (\underline {{E}} q: q \underline {{\mathrm {d e s p}}}: q) ] ⇒ f (\underline {{A}} r: r (\underline {{r d e s p}}): r) ] \ = {(6) a n d (7) } \ [ P ⇒ f P ] (9) \ \end{array}

In order to prove $R ⇒ L$ we now observe

\begin{array}{l} (\underline {{A}} q: q \underline {{\mathrm {d e s}}} p: [ q ⇒ Y ]) \ = {\text {p r e d . c a l c .} } \ [ (\mathrm {E q}: q \underline {{\mathrm {d e s p}}}: q) ⇒ Y ] \ = {(6) } \ [ P ⇒ Y ] \ = {(g) } \ [ P ⇒ Y ∧ f P ] \ ⇒ {\mathrm {d e f i n i t i o n} h \mathrm {a n d} k n a s t e r - T a r s k i } \ [ P ⇒ h Y ] \ ⇒ {(8) } \ [ p ⇒ h Y ] \ \end{array}

(End of Proof of Theorem 1.)

After the above exploration of the relation $q$ such that $-\left( {p ⇒ {f}^{ * }q}\right) -$ we shall apply our results to equation (4) with $f$ given by

[ p x \equiv - B v w | _ {p} (S, X) ]

we recall that with this choice for $f$ relation

in do B $\rightarrow$ S od, state q is a possible succes. sor of state $p$

Remark. Note that with this choice for $f$ , equation (4) with $[Y \equiv (\mathsf{B}\lor \mathsf{R})∧ (¬ \mathsf{B}\lor \mathsf{w}\mathsf{p}(\mathsf{S},\mathsf{t r u e}))]\mathsf{yields}$ our very first equation, of which $\mathsf{wp}(\mathsf{D}\mathsf{O},\mathsf{R})$ had been defined as the strongest solution; with $[Y \equiv \mathsf{B}\lor \mathsf{R}]$ , equation (4) yields our second equation, of which $\mathsf{wlp}(\mathsf{D}\mathsf{O},\mathsf{R})$ had been defined as the weakest solution. (End of Remark.)

With the above operational interpretation of sus, Theorem 0 enables us to give an operational interpretation of the predicate g true :

g true characterizes all (initial) states for which DO will not "continue" - i.e. will not lead to an infinite sequence of activations of $s$

Theorem 1 enables us to give an operational interpretation to $hY$ with $[Y \equiv ¬ B \lor wp(S, true)]$ . With this choice for $Y$ , $[q ⇒ Y]$ means that in state $q$ , either $DO$ has terminated or the activation of $S$ is guaranteed to terminate. From Theorem 1 we now see:

h (Bv w p (S, true)) characterizes all (initial) states for which DO will not "get stuck", i.e. will not lead to a nonterminating activation of

Our next choice for $Y$ is $[Y \equiv B \lor R]$ . With this choice for $Y$ , $[q ⇒ Y]$ means that in state $q$ , DO has not terminated or has terminated with $R$ holding. From Theorem 1 we now see:

h (BvR) characterizes all (initial) states for which DO will not terminate with IR.

This operational interpretation of $h(B \vee R)$ justifies its identification with $wlp(DO, R)$ . (See earlier Remark.)

The joint exclusion of continuing, getting stuck, and termination with $¬ R$ equivaies guaranteed termination with $R$ . From the above we see that the corresponding initial states are characterized by

g _ {f r u e} \wedge h (B v w p (S, f r u e)) \wedge h (B v R).

From (5) we conclude that the above equivaies

g ((B \vee R) \wedge (¬ B \vee w p (S, t r u e)))

its operational interpretation justifies its identi-fication with $\operatorname{wp}\left( {{DO},R}\right)$ . (See earlier Remark.)

For the sake of completeness we remark

• h B c h a r a c t e r i z e s all (i n i t i a l) s t a t e s for which D0 will not terminate
• g B c h a r a c t e r i z e s all (i n i t i a l) s t a t e s for which D0 will get stuck $h\left( {B ∧ {wp}\left( {S,\text{true}}\right) }\right)$ characterizes all (initial)

states for which do will continue

The well-known relation

[ w p (D O, R) \equiv w l p (D O, R) ∧ w p (D O, t r u e) ]

takes on account of the above the form

\begin{array}{l} [ g ((B \vee R) \wedge (B \vee w p (S, t r u e))) ] = \ h (B \vee R) \wedge g (I B \vee w p (S, t r u e)) ] , \ \end{array}

which is confirmed by (5).

Finally we check that it is impossible to guarantee nontermination and termination, i.e. that

$\left\lbrack {h\mathrm{ B} ∧ \mathrm{{wp}}\left( {\mathrm{D}\mathrm{O},\text{ true }}\right) \equiv {\text{ false }}\right\rbrack ,\mathrm{{or}},\mathrm{{by}}$ the above and (5),that $\left\lbrack {g\left( {\mathrm{B} ∧ \mathrm{{wp}}\left( {\mathrm{S},\text{ true }}\right) }\right) \equiv {\text{ false }}\right\rbrack$ .

Substitution of $g$ ’s argument for $Y$ in (4)

y i e l d s

X: [ X \equiv B ∧ w p (S, t r u e) ∧ (¬ B \lor w p (S, X)) ]

or

X: [ X \equiv B ∧ w p (S, X) ]

which has indeed false as its strongest solution.

6 April 1984

drs. C.S. Scholten

Scientific Adviser

Philips Research Laboratories

5600 JA EINDHOVEN

The Netherlands

prof.dr.Edsger W.Dgksha

Burroughs Research Fellow

Plataansstraat 5

5671 AL NUENEN

The Netherlands