A formal program derivation for the record

A formal program derivation for the record

The program imptest satisfy the specification

If $N$ : int ${ N ≥ 0} ;b\left( {i : 0 ≤ i < N}\right)$ array of bool

; 1[x:boo]

i'mpdef ${ R : x \equiv \left( {\underline{A}{i}{1}j : 0 ≤ i < j < N : {b}{i} ⇒ {b}_{j}}\right) }$

11

Legenda for the unfamiliar The bracket pairs I...J1 delineate scopes for the variables. The environment of imptest is declared in two stages: in the outer block the constants, in the inner block the variables. The postcondition is given the name R . (End of legenda for the unfamiliar.)

To start with, we massage the post condition:

R

= {\text {e l i m i n a t i o n} o f ⇒ }

x \equiv (\underline {{A}} i, j: 0 ≤ i < j < N: - b i \vee b j)

= {\mathrm {s e p a r a f i o n o f q u a n t i f i c a t i o n s} }

x \equiv (\underline {{A}} j: 0 ≤ j < N; (\underline {{A}} i: 0 ≤ i < j: ¬ b i \vee b j))

= {v d i s t r i b u t e s o v e r A }

x \equiv (\underline {{A}} j: 0 ≤ j < N: (\underline {{A}} i: 0 ≤ i < j: ¬ b i) \vee b j)

= {\mathrm {n a m i n g a n d p a r a m e t e r i z i n g t h e u n i v e r s a l q u a n t i f i c a t i o n s} } x \equiv H N

where ${H}{n} \equiv \left( {\underline{A}}{j} : 0 ≤ j < n : k\mathbf{j} \vee b\mathbf{j}}\right)$ (1)

k j \equiv (\underline {{A}} i: 0 ≤ i < j: ¬ b i) \tag {2}

Note. Like b, H and K are treated as functions, and functional application is given the greatest binding power. (End of Note.)

From (1) we deduce ${\mathrm{property~of~universal~quanhi}$

H (n + 1) \equiv H _ {n} \wedge (k n \vee b n) (3 a)

and similarly from (2)

K (n + 1) \equiv K n \wedge ¬ b n . (3 b)

This suggests as invariant

P: (x \equiv H n) ∧ (y \equiv K n) ∧ (0 ≤ n ≤ N), \tag {4}

for which we observe

(i) $x,y,n \mathrel{\text{:=}}$ true, true, 0 establishst $P{$ vacuously (ii) $n≠ N\rightarrow$

x, y, n := x \wedge (y \vee b (n)), y \wedge ¬ b (n), n + 1

maintains $P{ \left( 3\right)$ and(4)\$

(iii) $n = N ∧ P ⇒ R \left{ \left( 0\right) and \mid 4} \right}$ .

Before rushing into program construction, however, we observe that ${(0),(1),$ and $(4)}$

[\text{而} ∧ \text{P} ⇒ \text{R}\text{,}]

which yields in combination with (iii)

$(n = N \vee n) \wedge P ⇒ R,$

so the guard of (ii) can be strengthened to

$n ≠ N ∧ x$ ,i.e. to consider,instead of (ii)

$\left( v \right) n ≠ N ∧ x \rightarrow$

x, y, n := x \wedge (y \vee b (n)), y \wedge ¬ b (n), n + 1,

which maintains $P$ a forderiori. The observation that(v) can be simplified to

\begin{array}{l} n ≠ N ∧ x \rightarrow \ x, y, n := y \vee b (n), y \wedge ¬ b (n), n + 1 \ \end{array}

yields for impfesst the solution:

$\left\lbrack {y : \text{bool}}\right\rbrack ;n : \text{int}$

\begin{array}{l} ; x, y, n := true, true, 0 {\mathcal {P} } \ ; do n ≠ N ∧ x \rightarrow \ x, y, n := y \vee b (n), y \wedge ¬ b (n), n + 1 {P } \ od {(n = N \vee 7 x) \wedge P, h e n c e } \ \mathbb {1} {R } \ \end{array}

on account of the last term of $P$ ,termination is obvious.

In the above I have assumed the reader familiar with (de Morgan's law and) the central theorem about repetitions - i.e. how to use invariants and how to prove termination.. In dealing with a specific program, one should concentrate on what is specific to that program.

When I showed the above derivation to Dr. H. Richards Jr., he justifiably remarked that

I had violated my own principle of developing pro- gram and correctness proof hand in hand: "You did almost all of the proof beforehand." Proof development usually leads program derivation; what Richards had observed is to be expected with programs as small as this one.

I must draw attention to the notational benefit we derived from the introduction of the functions H and K . To the uninitiated it may seem that, at the bottom of p.o, they have just been pulled out of a hat and that, on p.i, they miraculously emerge to be precisely what we needed. To the experienced, however, their introduction is almost a routine job, and I did not want to clog this presentation of the program with heuristics (which are quite a different matter).

Furthermore I must draw attention that we did not need to mention a single special case (say: $N = 0$ , $N = 1$ , or all the $b(i)$ false). I mention this because avoidable case analyses should be avoided: they tend to lengthen the program text as well as the justifying argument and are a source of errors.

One final remark, be it of a different order. The omission of parentheses, possible thanks to the high priority of functional application, was certainly a convenience, but I observe myself

becoming more and more doubtful about the convention of representing such a fundamental operation as functional application "invisibly" by just juxtaposition. Were we to indicate it explicitly, a very small symbol should be chosen in view of its high binding power. I can only think of the period: this would lead to b.i., H.n, but also to H.(n+1). I expect I shall consider the suggestion seriously.

Austin, 8 Sep. 1984

Prof. dr. Edsger W. Dgiksha Department of Computer Sciences The University of Texas at Austin AUSTIN, TX 78712-1188 U.S.A.