EWD249 - 17

"integer r, dd, q;
 r:= a; dd:= d; q:= 0;
 while dd ≤ r do dd:= 2 * dd;
 while dd ≠ d do
   begin dd:= dd / 2; q:= 2 * q;
         if dd ≤ r do begin r:= r - dd; q:= q + 1 end
   end

assigns to q the value of the corresponding quotient. The proof can be established by observing the invariance of the relation

a = q * dd + r   .

(I owe this example to my colleague N.G.de Bruijn.)

Remark 2. In the subsection "On mathematical induction." we have proved the Linear Search Theorem. In the previous proof we have used another theorem about repetitions (a theorem that, obviously, can only be proved by mathematical induction, but the proof is so simple that we leave it as an exercise to the reader),viz. that if prior to entry of a repetition a certain relation P holds, whose truth is not destroyed by a single execution of the repeated statement, then relation P will still hold after termination of the repetition. This is a very useful theorem, often allowing us to bypass an explicit appeal to mathematical induction. (We can state the theorem a little bit sharper;in the repetition

"while B do S"

one has to show that S is such that the truth of

P and B

prior to the execution of S implies the truth of

P

after its execution.)

Remark 3. As an exercise (for which acknowledgement is due to James King, CMU, Pittsburgh, USA) for the reader, prove that with integer A, B, x, y and z and

A > 0  and B ≥ 0

after the execution of the program section