EWD249 - 74

linemark: {while f ≤ x do {sym[f]:= space; f plus 1};
           sym[x]:= mark}

a version which guarantees that whenever "sym[x]:= mark" is executed, the relation "x < f" will always be satisfied: it is precisely the function of the first line to see to this. The reader is invited to try to understand both versions of linemark and to compare both reasonings. He will then agree with my judgement that the original version is lousy.

The second version jumped into my mind on account of the following observation. The conditional clause

"if B do S"

is used in programs in two different ways. On the one hand we have the applications, in which the execution of the statement S does not invalidate the truth of B, on the other hand we have the situations in which the execution of the statement S is guaranteed to invalidate the truth of B. In the latter case, it is the function of the conditional statement to ensure that after its execution B will not hold. It is then, essentially, a shortcut for

"while B do S",

which has the property of invalidating the truth of B (provided that it stops), but the justification of the shortcut requires a separate proof that the repeated statement will be executed at most once. (In "A first example of step-wise program composition" we did not bother to introduce this shortcut on level 2b4(4) where we wrote

"while "ord too small" do "increase ord by one"  ;

here a conditional clause would have done the job!)