EWD249 - 32

and

        "j:= 0; equal:= true;
         while j ≠ N and equal do
             begin j:= j + 1; equal:= (X[j] = Y[j]) end"    (4)

Program (4) differs from program (3) in that repetition is terminated as soon as a pair-wise difference has been detected. For the same input the number of repetitions may differ in the two programs and therefore the programs are only comparable in our sense as long as the last two lines of the programs are regarded as describing a single action, not subdivided into subactions. But what is their relation when we do wish to take into account that they both end with a repetition? To find this out, we shall prove the correctness of the programs.

On the arrays X and Y we can define of 0 ≤ j ≤ N the N + 1 functions EQUAL_j as follows:

for j = 0        EQUAL_j = true        ,
for j > 0        EQUAL_j = EQUAL_{j-1} and (X[j] = Y[j])                 (5)

In terms of these functions it is required to establish the net effect

        equal = EQUAL_N   .

Both programs maintain the relation

        equal = EQUAL_j                            (6)

for increasing values of j, starting with j = 0.

It is tempting to regard both programs (3) and (4) as alternative refinements of the same (abstract) program (7):

        "j:= 0; equal:= EQUAL_0;
         while "perhaps still: equal ≠ EQUAL_N" do
             begin j:= j + 1; "equal:= EQUAL_j" end"          (7)

in which "perhaps still: equal ≠ EQUAL_N" stands for some sort of still open primitive. When this is evaluated

        equal = EQUAL_j

will hold and the programs (3) and (4) differ in that they guarantee on different