Constructing the Binary Search once more

Constructing the Binary Search once more

There are several reasons for writing this note: firstly I found a way of being more explicit than before about the design considerations, and this I want to have recorded, secondly it is an experi- ment in presenting the evolution of a design.

A, the program should establish

${R0} : \;$ present $\equiv \left\langle {\exists i : 0 \leq i < N : A\left\lbrack i\right\rbrack = X}\right\rangle$

When the value X does occur in array A and the program therefore should see to it that present is set to true , it is hard to see how this can be justified without at the same time establishing where in the array A value X occurs, i.e., for some variable i the program will establish

(0) $A[i] = X,$

but as intermediate target this is too strong, for no such i exists when X does not occur in array A. In the latter case we might have to be content with establishing

$A\left\lbrack i\right\rbrack < X < A\left\lbrack {i + 1}\right\rbrack$

i.e. identifying the two nearest neighbours of $X$ . Since the algorithm must be able to cope with both presence and absence of $X$ ,we suggest the combination of (0) and (1)

${R}_{1} : \;A\left\lbrack i\right\rbrack \leq X < A\left\lbrack {i + 1}\right\rbrack$

as a more realistic target. (Note that we have ${R}_{1} \equiv \left( 0\right) v\left( 1\right)$ if $A\left\lbrack i\right\rbrack < A\left\lbrack {i + 1}\right\rbrack$ .)

Summarizing. We are considering a program of the form

(2) ${ C} 1\left\lbrack {\text{var}i : \text{int}}\right\rbrack$ ; "establish ${R}_{1}$ " $\left{ {R + }\right}$ present $\Rightarrow A\left\lbrack i\right\rbrack = X$

We introduced the as yet unknown precondition C to cater for the possiblity that we won't be able to establish R1 under all circumstances; a C different from true means that ours is still a partial design.

It stands to reason to expect that larger values of $N$ might require larger computation times and that, therefore, our program contains a repetitive construct. Program (2) tells us that repetition occurs in "establish $R_1$ ". We make the simplest assumption, viz. that $R_1$ is established

by the completion of that repetition, which means that we must choose an invariant that is a generalization of R1 . Again we choose (in principle) the simplest device, viz. that of replacing a constant by a fresh variable, j say. Replacing the constant 1 by j would yield for the invariant the conjunct

$$ A [ i ] \leqslant X < A [ i + j ] $$

and for the guard of the repetition the expression

Because $R$ is really the conjunction of two conditions, it is preferable to replace the whole subexpression $i + 1$ by $j$ . This yields for the invariant $P$ the conjunct(s)

$A\left\lbrack i\right\rbrack \leq \times \;X < A\left\lbrack j\right\rbrack$

and for the repetition the guard

$j \neq i + 1$

Remark from the point of view of information theory, the choice just made is immaterial: if $p,q,r$ satisfy $p + q = r$ , the values of any two of them determine the value of the third. From the point of view of disentangling the argument, the choice is significant: now each variable is associated with its own con

junct to be maintained. (End of Remark.)

We postpone the discussion of how to maintain (3) during the repetition and ask ourselves first how we can establish it at the initialization of $\mathfrak{z}$ j. Looking at R0 -the only place where specific subscript values have been mentioned- I can think of only one initialization, viz.

$$ i, j := 0, N $$

which only establishes (3) provided we have

$A\left\lbrack 0\right\rbrack \leq X\;X < A\left\lbrack N\right\rbrack$

We meet this condition by defining $c$ to be equal to (5) , Summarizing, we are in the mean time considering a program of the form

(6) ${ C} 1\left\lbrack {\operatorname{var}i : \operatorname{int}}\right\rbrack$ ; II var j: int; $i,j \mathrel{\text{:=}} 0,N{ P}$ ; do $j \neq i + 1 \rightarrow$ ${ P \land j \neq i + 1}$ "adjust ${i}{2}{j}^{\prime \prime }{ P}$ $\left. \begin{array}{l} \text{ od } \ \text{ od } \ \text{ if }\left\lbrack {R}{1}\right\rbrack \ \ \text{ if }\left\lbrack {R}_{1}\right\rbrack \ \ \text{ else } \end{array}\right}$ $\vdots { R}$ present: $A\left\lbrack i\right\rbrack = X$

We now turn to the design of such an "adjust $i,j$ " that we can assure termination of the

repetition, i.e. we are looking for a variant function $t$ that is decreased by "adjust $i,j$ " and is bounded from below. The fact that upon termination $j - i$ equals 1 while initially it equals $N$ ,which is at least 1 but is allowed to be much larger,suggests to try

$t = j - i$

and to include in $P$ the conjunct

(8) $i < j$

so as to ensure that it is bounded from below.

Now we take a seemingly bold step: we pro- pose for "adjust $i,j$ " an inner block of the form

${ i + 1 < j} \left\lbrack {\operatorname{var}h : \operatorname{int}h}\right\rbrack$

$$ \begin{array}{l} h := \dots {0 } \ i: i f \dots \rightarrow {Q _ {i} } i := h {i < j } \ {\cdot \dots \rightarrow {Q j } j := h {i < j } \ | \frac {f _ {i}}{{i < j }} \ \end{array} $$

Remark I wrote "seemingly bold", and I think rightly so, for the only constraint implied by (9) is that a single execution of "adjust $i,j$ modi-fies either $i$ or $j$ , and since (3) presents independent constraints on $i$ and $j$ , we can live with that: invariance of (3) will not re-

quire a single execution of "adjust $\mathrm{i}$ j" to modify

We now calculate Qj and Qj from the requirements that decrease and remain

positive

$= {$ definitions of $+$ and statement in question

$$ [ i := h ] (j - i) < j - i \wedge [ i := h ] (i < j) $$

[\left{ \begin{array}{ll} \text{substitution operator twice } \ \end{array}\right} ] $j - h < j - i,h < j$ [\text{algebra}} ]

$$ i < h \land h < j $$

$\equiv \;$ {qj}

$$ [ j := h ] (j - i) < j - i \land [ j := h ] (i < j) $$

[\left. \equiv \left{ \begin{array}{ll} \text{substitution operator twice} \ \end{array}\right} ] $h - i < j - i$ $i < h$ [\text{a}\left( {x,y}\right) = \left{ \begin{array}{ll} a & \text{ 若 }y > 0 \ b & \text{ 若 }y < 0 \end{array}\right. ]

$$ h < j \land i < h $$

i.e., we find for Qi and Qj the same predicate

$c < h \land h < j$

In response to this observation we choose (10) for $Q$ ,the precondition for the alternative construct. We point out that since here $C$ and $j$ are at least 2 apart,an $h$ satisfying (10)

exists. We leave to the reader the verification that, without any need to strengthen guards of the alternative construct, the conjunct $\mathrm{osc} \land j \leq N$ can be added to the invariant $P$ .

As far as $i, j$ are considered,we have reached the program

(11) ${ 0 < N} \mid \left\lbrack {\operatorname{var}i : \operatorname{int}}\right\rbrack$

31

$$ \begin{array}{l} i \in [ \mathrm {v a r} j: i n t \ i, j := 0, N {P } \ i + 1 \neq j \rightarrow {P \land i + 1 < j } \ 1 [ \text {v a r h}; \text {i n t} \ ; h := a v g. i j {P \wedge i < h < j } \ i f \mathrm {t r u e} \rightarrow i := h [ P ] \ \iiint_ {D} \mathbf {P} \rightarrow j := h (P) \ \begin{array}{l} \frac {p _ {i}}{I} \ ] 1 \quad {\cdot } \end{array} \ \mathrm {o d} {P \wedge i + 1 = j } \ ] 1; \mathrm {p r e s e n t} := A [ i ] = X \ \end{array} $$

with $P$ equal to $0 \leq i \land {ij} \land j \leq N$ ,and as only requirement that avg. i.j yields a value strictly between i and j . No matter what avg we choose, nor how the nondeterminacy of the alternative construct is resolved, the repetition terminates, creating the state $i + 1 = j$ .

And now the time has come for the postponed discussion of how to maintain (3), that is

$$ A [ i ] \leq X \land X < A [ j ] $$

as part of the invariant $P$ . The first conjunct can only be falsified by the only assignment to i , viz. $i = h$ ,but the Axiom of Assignment tells us that its preassertion $\left{ {A\left\lbrack h\right\rbrack \leq X}\right}$ implies its postassertion $\left{ {A\left\lbrack i\right\rbrack \leq X}\right}$ . Strengthening the preceding guard to the precondition does the job. Similarly the assignment $j : = h$ is prevented from falsifying $P$ by guarding it by $X < A\left\lbrack h\right\rbrack$ . In other words, it suffices for the invariance of (3) to replace in the above program the alternative construct by

$$ \begin{array}{r l}{\mathrm {i f} \quad}&{A [ h ] \leq X \rightarrow i := h}\{\mathrm {I I}}&{X < A [ h ] \rightarrow j := h}\{\mathrm {p i}}&{}\end{array} $$

and to our joy we observe that the disjunc tion of the strengthened guards is still equal to true , so we did not introduce the danger of abortion.

Because of $0 \leq i < h < j \leq N$ ,access to the array $A$ is in the repetition restricted to $A\left\lbrack h\right\rbrack$ for $0 < h < N$ ; in the setting of "present" $A\left\lbrack o\right\rbrack$ may be accessed. Thus access is restricted to $A\left\lbrack i\right\rbrack$ for $0 \leq i < N$ ,the range of the quanti

fication in Ro , our problem statement. As a con- sequence we need not bother about $X < A\left\lbrack N\right\rbrack$ , the second conjunct of (5), the proposed pre- condition C for the whole program, since nothing prevents us from making $X < A\left\lbrack N\right\rbrack$ true by definition, say by defining $A\left\lbrack N\right\rbrack = + \infty$ . With that symbolic value the program is certain to establish $R$ provided also (5)'s first conjunct $A\left\lbrack 0\right\rbrack \leq X$ holds. But what if $X < A\left\lbrack 0\right\rbrack$ ? Well, ${R}_{1}$ may not be established,but the repetition terminates with $0 \leq i < N$ -because it does so independently of $X$ and $A$ - and then "present" is set to false as it should.

*

Well, that's it. The "experiment in presenting the evolution of a design", which was mentioned in the first paragraph, was abandoned, I'm afraid. I wanted to develop the program without recording all the successive versions as that involves so much rewriting, and thought I could do that by writing a program text with, in the assertions, names of predicates which would be developed off line. I more or less did so with P but halfway the text I felt that the question of how to simulate chalk and blackboard in print is a separate issue, and that is how it got abandoned.

I did like program (11), in particular before I had inserted the assignment to "present" at the end - this insertion was done later - , because it nicely shows how the i, j- mani- pulation -and in particular the termination- is independent of $X$ and A . It is now hard to believe that I have seen binary searches whose termination depended on A being sorted or on how rounding took place in calculating avg. i, j ! Besides this very clear separation of concerns I liked the calculations of Qi and Qj which yield the same predicate, but with the conjuncts interchanged. It is no accident that the development concentrated on j-i, i.e. on its lower bound and on its decrease, for this is the only place where i and j occur in com- bination, all other conjuncts in P depending either on i or on j :

Austin, 13 November 1999

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