EWD249 - 9

the value of dd, but leaves r unchanged, the relations

                0 ≤ r < 2 * dd                                   (2)

will hold. Now we distinguish two mutually exclusive cases.

1. dd ≤ r. Together with (2) this leads to the relations

                dd ≤ r < 2 * dd   ;                              (3)

In this case the statement following do will be executed, ordering a decrease of r by dd, so that from (3) it follows that eventually

                0 ≤ r < dd        ,

i.e. (1) will be satisfied.

2. non dd ≤ r (i.e. dd > r). In this case the statement following do will be skipped and therefore also r has its final value. In this case "dd > r" together with (2), which is valid after the execution of the first statement leads immediately to

                0 ≤ r < dd

so that also in the second case (1) will be satisfied.

Thus we have completed our proof of the invariance of relations (1), we have also completed our example of enumerative reasoning, conditional clauses included.

On mathematical induction.

I have mentioned mathematical induction explicitly because it is the only pattern of reasoning that I am aware of that eventually enables us to cope with loops (such as can be expressed by repetition clauses) and recursive procedures. I should like to give an example.

Let us consider the sequence of values

                d_0, d_1, d_2, d_3,......                         (1)

given by

for i = 0        d_i = D                                        (2a)
for i > 0        d_i = f(d_i-1)                                 (2b)