EWD249 - 42

By identifying k as the number of primes found and by verifying that our our first prime number (= 2) is indeed the smallest prime number larger than 1 (= the initial value of j), the correctness of 2b1(2) is easily proved by mathematical induction (assuming the existence of a sufficient number of primes).

Description 2b1(2) is a perfect program when the operation described by "increase j until next prime number" -call it 2b1(2)a- occurs among the repertoire, but let us suppose that it does not. In that case we have to express in a next refinement how j is increased (and, again, preferably nothing more). We arrive at a description of level 2b2(2)

2b1(2)a  =
begin boolean jprime;
      repeat j:= j + 1;
             "give to jprime the meaning: j is a prime number"
      until jprime
end

Remark. Here we use the repeat-until clause in order to indicate that j has always to be increased at least once.

Again its correctness can hardly be subject to doubt. If, however, we assume that the programmer knows that, apart from 2, all further prime numbers are odd, then we may expect him to be dissatisfied with the above version because of its inefficiency. The price to be paid for this "lack of clairvoyance" is a revision of version 2b1(2). The prime number 2 will be dealt with separately, after which the cycle can deal with odd primes only. Instead of 2b1(2) we come to

2b1(3):
begin integer k,j; p[1]:= 2; k:= 1; j:= 1;
      while k < 1000 do
            begin "increase odd j until next odd prime number";
                  k:= k + 1; p[k]:= j
            end
end

where the analogous refinement of the operation between quotes -"2b1(3)a" say- leads to the description on level 2b2(3):