EWD249 - 46

level 2b2(4):
2b1(4)a   =
begin boolean jprime;
      repeat "increase j with two";
             "give for odd j to jprime the meaning: j is a prime number"
      until jprime
end;
2b1(4)b   =  2b2(4)b

expressed in terms of
2b2(4)b     still meaning "set j to one"
2b2(4)c     "increase j with two"
2b2(4)d     "give for odd j to jprime the meaning: j is a prime number"  .

It is only at the next level that we need to talk about ord. Therefore we now write

level 2b3(4):   integer ord;
2b2(4)b   =
begin j:= 1; "set ord initial" end;
2b2(4)c   =
begin j:= j + 2; "adjust ord" end;
2b2(4)d   =
begin integer n; n:= 2; jprime:= true;
      while n < ord and jprime do
      begin "give to jprime the meaning: p[n] is not a factor of j";
            n:= n + 1
      end
end

expressed in terms of
2b3(4)a     "set ord initial"
2b3(4)b     "adjust ord"
2b3(4)c     "give to jprime the meaning: p[n] is not a factor of j".

In our next level we give two independent refinements. (Note. We could have given them in successive levels, but then we should have to introduce an arbitrary ordering to these two levels. We could also try to treat the refinements separately