EWD249 - 15

An example of a correctness proof.

Let us consider the following program section, where the integer constants a and d satisfy the relations

                a ≥ 0    and    d > 0    .

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

To apply the Linear Search Theorem (see Section "On our mental aids", sub-section "On mathematical induction") we consider the sequence of values given by

for i = 0        dd_i = d
for i > 0        dd_i = 2 * dd_i-1
from which       dd_n = d * 2^n                                        (1)

can be derived by normal mathematical techniques, which also tell us that (because d > 0) for finite r

                dd_k > r

will hold for some finite k, thus ensuring that the first repetition terminates

with            dd = d * 2^k        .

Solving the relation

                d_i = 2 * d_i-1

for d_i-1 gives      d_i-1 = d_i / 2

and the Linear Search Theorem then tells us, that the second repetition will also terminate. (As a matter of fact the second repeated statement will be executed exactly the same number of times as the first one.)

At the termination of the first repetition,