A detailed derivation of a very simple program

A detailed derivation of a very simple program

We are going to derive a program "test all true", satisfying the following specification:

11 con N: int; con f: int → bool; var x: bool ；test all true R: x ≡ <k:0≤k ∧ k<N: f.k>3

Our first step is to rewrite the right-hand side of $R$ as a function (whose properties we'll subsequently exploit) of some argument(s). Since functions of integers are simpler than functions of functions, we consider the function $f$ as a constant, but do consider the right-hand side of $R$ a function of the two bounds of the range, that is, we rewrite the post condition

R: $x \equiv {H.0.N}$

where $H$ is given by

(H) $\;h \equiv \left\langle {\forall k : i \leq k \land k < j : f \cdot k}\right\rangle$

*

Our next step is -unavoidably!- the investigation of the (hopefully exploitable) properties of the function $+1$ ,just introduced. Standard application of predicate calculus (and nothing else but lemmata like

$$ k < j \vee k = j \equiv k < j + 1) $$

yields the following three properties of $H$

$\left( 1\right) \;i \geq j \Rightarrow H.i.j$ $i < j \Rightarrow \left( {H.\left( {i + 1}\right) .j \land f;i \equiv H.i,j}\right)$ (3) $i < j \Rightarrow \left( {H,i.\left( {j - 1}\right) \land f.\left( {j - 1}\right) \equiv H,i,j}\right)$

In (1) we recognize "bases" - (1) holds for all $i,j$ . In (2) and (3) "steps".

Heading for a repetition, our third step is -unavoidably!- the choice of an invariant that can be (i) initialized , (ii) maintained, and (iii) used to conclude R . Postponing our concerns regarding (ii), we observe that - thanks to Leibniz's Principle - we can initialize

$$ H. i j \equiv H. 0. N $$

• viz. by $i, j \mathrel{\text{:=}} 0,N -$ but that the left-hand side has to be generalized so as to contain x in such a fashion that we can conclude R . We choose for invariant P o A P

[{H}_{i} \cdot j \land x \equiv {H.0.N}]

${P}_{1} : \;0 \leq i \cdot j \leq N$

Ad Po we remark that the alternative left-hand

sides H.i.j v x and H.i.j = x would have given invariants as easily initialized as Po. But in order to conclude R, i.e.

$$ x \equiv H. 0. N $$

from (H.i.j op x) = H.0.N ,

the known value of H.ij should be the unit element of op . Since (1) tells us that the known value of H.ij is true, this rules out the disjunctio. In view of (2) and (3), the equivalence seems to lead to an invariant hard to maintain, and hence the conjunction in - PO .

Our fourth step is to determine under what additional condition the invariant implies $R$ . To this end we observe

$$ = \begin{array}{l} R \ {\mathrm {d e f i n i t i o n o f} R } \ x \equiv H. 0. N \end{array} $$

$$ \begin{array}{r l} {=} & {{\mathrm {P O} }} \ & {\times \equiv x \wedge H _ {i j}} \ {=} & {{\mathrm {p r e d . c a l c .} }} \ & {\times \vee H _ {i j}} \end{array} $$

$$ \Leftrightarrow \left{ \begin{array}{l} (1) \ 7 \times v \quad i \geq j \end{array} \right., $$

after which observation we decide to use

the negation of the last expression, i.e.

(4) $x \land i < j$

as guard.

Our fifth step is to derive the command(s) guarded in the repetition. In order to use (2) we consider a guarded command that comprises $i \coloneqq i + 1$ and leaves $j$ constant. (Note that $i \coloneqq i + 1$ and $j \coloneqq j - 1$ work towards falsification of $i < j$ , and that is nice for termination.) We consider for as yet unknown $E$ the requirement that

$$ X \wedge i < j \rightarrow i, X := i + 1, E $$

leave Po invariant. We observe

$$ w p. (i, x := i + 1, E). P _ {0} $$

$$ \begin{array}{l} = \quad {d e f. := ; d e f. P _ {0} } \ H. (i + 1). j \wedge E \equiv H. 0. N \ = {P _ {0}, e x h y p o t h e s i } \ H. (i + 1). j \wedge E \equiv H. i. j \wedge x \ = {\times f r o m t h e g u a r d } \ H _ {i} (i + 1). j \wedge E \equiv H _ {i}. j \ = {i < j f r o m t h e g u a r d, (2) } \ H _ {0} (i + 1), j \wedge E \equiv H _ {0} (i + 1), j \wedge f _ {0} i \ \Leftrightarrow {L e i b n i z } \ E \equiv f. i \ \end{array} $$

i.e. the guarded command

$$ x \wedge i < j \rightarrow i, x := i + 1, f. i $$

leaves ${P}{0}$ invariant. Similarly,we derive from the requirement that ${P}{0}$ is maintained that the guarded command

$$ x \wedge i < j \rightarrow j, x := j - 1, f (j - 1) $$

meets the requirement. Hence a solution is

test all true;

115 var i,j:int; i,j:=0,N{inv:Pi,bnd j-i}

$$ \begin{array}{l} i, \underline {{d o}} x \wedge i < j \rightarrow i, x := i + 1, f _ {i} i \ [ \cdot ] x \wedge i < j \rightarrow j, x := j - 1, f _ {i} (j - 1) \ \operatorname {o d} {P _ {0} \wedge (i x \vee i _ {\ge j}), h e n c e } \ \end{array} $$

$$ \left. \right] \left{\mathbf {R} \right} $$

Remark In the context of this note it is not interesting that in the above program the nondeterminacy can be reduced (by removal of one of the guarded commands). Nondeterminacy can always be reduced. (End of Remark.)

Cognoscenti recognize an Eindhoven influenza, in particular of Anne Kaldewajj, who did much to establish the superiority of the tail invariant, and of Wim H.J. Feijen, who taught

me (in WF155) how to derive the guard $x > 1 < j$ "from outside in", that is by confronting the postcondition with the invariant. These influences are gratefully acknowledged.

This note has been written for the sake of the fifth step, in which the repeatable statement is derived. (I don't remember ever having done it that way.)

The way in which nondeterminacy entered this program was a surprise; it was a pleasure to see that it almost dictated a tail invariant.

Austin, 18 October 1993

PS The weakest solution of the equation

$$ X: [ X \wedge Y \Rightarrow Z ] $$

is $Y \Rightarrow Z\;$ . If helps to know this. (End of PS.)

prof. dr. Edsger W. Dyrkstra Department of Computer Sciences The University of Texas at Austin Austin, TX 78712 - 1188 USA