EWD249 - 33

criteria that "equal" will have its final value EQUAL_N.

In program (3) the criterion is very naive, viz.

        j = N.

At the beginning of the repeated statement

        equal = EQUAL_j

still holds. After the execution of "j:= j + 1" therefore

        equal = EQUAL_{j-1}

holds and the assignment statement

        "equal:= equal and (X[j] = Y[j])"

is now a straightforward transcription of the recurrence relation (5).

To come to program (4) some analysis has to be applied to the recurrence relation (5), from which can be derived (by mathematical induction again) that EQUAL_j = false implies EQUAL_N = false, and therefore EQUAL_j = false implies EQUAL_j = EQUAL_N. If this situation arises, the equality "equal = EQUAL_N" can also be guaranteed and this leads to program (4). The set of (sub)computations the repeated statement has to cope with in program (4) is restricted to those with the initial state "equal = true" and therefore in program (4) the assignment "equal:= EQUAL_j" can be abbreviated to

        "equal:= (X[j] = Y[j])"     .

And now it is clear why the introduction of (7) as an abstraction of (3) and (4) was misleading. With "perhaps still: equal ≠ EQUAL_N" we have stated the meaning of truth and falsity of a boolean expression without stating the expression itself and that was very tricky. We have tried to interpret (7) as a program in which part of the sequencing at its own level was undefined and varying over its refinements. As a result we have tried to view the last lines of (7) as a model for the last lines of both (3) and (4), but this was misleading because the computations to be evoked by them cannot be brought into a one-to-one correspondence.

So much about programs that we consider as incomparable. Examples of comparable programs will be encountered in the following sections. A final remark: we have stated