EWD249 - 10

where D is a given value and f a given (computable) function. It is asked to make the value of the variable "d" equal to the first value d_k in the sequence that satisfies a given (computable) condition "prop". It is given that such a value exists for finite k. A more formal definition of the requirement is to establish

the relation        d = d_k                                      (3)

where k is given by the (truth of the) expressions

                prop(d_k)                                        (4)
and             non prop(d_i)   for all i satisfying 0 ≤ i < k     (5).

We now consider the following program part:

                "d:= D;
                while non prop(d) do d:= f(d)"                   (6)

in which the first line represents the initialization and the second one the loop, controlled by the (hopefully self-explanatory) repetition clause while...do. (In terms of the conditional clause if...do, used in our previous example, a more formal definition of the semantics of the repetition clause is by stating that

                "while B do S"

is semantically equivalent with

                "if B do
                    begin S; while B do S end"

expressing that "non B" is the necessary and sufficient condition for the repetition to terminate.)

Calling in the construction "while B do S" the statement S "the repeated statement" we shall prove that in program (6):

after the n-th execution of the repeated statement will hold (for n ≥ 0)

                d = d_n                                          (7a)
and             non prop(d_i)   for all i satisfying 0 ≤ i < n   .     (7b)

The above statement holds for n = 0 (by enumerative reasoning); we have to prove (by enumerative reasoning) that when it holds for n = N (N ≥ 0), it will also hold for n = N + 1.