EWD249 - 16

dd = dd_k

and therefore,

0 ≤ r < dd                                                       (2)

holds. As shown earlier (Section "On our mental aids.", subsection "On enumeration") the repeated statement of the second clause leaves this relation invariant. After termination (on account of "while dd ≠ d do") we can conclude

dd = d

which together with (2) gives

0 ≤ r < d                                                        (3)

Furthermore we prove that after the initialisation

dd ≡ 0 mod(d)                                                    (4)

holds; this follows, for instance, from the fact that the possible values of dd are -see (1)-

d * 2^i      for 0 ≤ i ≤ k .

Our next step is to verify, that after the initial assignment to r the relation

a ≡ r mod(d)                                                     (5)

holds.

1. It holds after the initial assignments.

2. The repeated statement of the first clause ("dd:= 2 * dd") maintains the invariance of (5) and therefore the whole first repetition maintains the validity of (5).

3. The second repeated statement consists of two statements. The first ("dd:= dd/2") leaves (5) invariant, the second one also leaves (5) invariant for either it leaves r untouched or it decreases r by the current value of dd, an operation which on account of (4) also maintains the validity of (5). Therefore the whole second repeated statement leaves (5) invariant and therefore the whole repetition leaves (5) invariant. Combining (3) and (5), the final value therefore satisfies

0 ≤ r < d    and    a ≡ r mod(d)

i.e. r is the smalles non-negative remainder of the division of a by d.

Remark 1. The program