An intriguing example.

In the following all variables and all elements of the infinite arrays f [0...] and g[0...] are of type natural number.

Array f is ascending, i.e.

 (A x : x≥0 : f [x] ≤ f [x+1]) (0)
and unbounded, i.e.
 (A y : y≥0 : (E x : x≥0 : f [x] > y)) (1)

As a result of (1)

 prog 0: do f [x] ≤ y → x := x+1 od
terminates. Also — obviously —
 prog 1: do f [x] > y → g[y]:= x; y := y+1 od
terminates. The “combined” program
 x, y := 0,0; do f [x] ≤ y → x := x + 1; ⫿ f [x] > y → g[x] := x; y := y+1 od
obviously fails to terminate. Hence, x and y are both unbounded: more and more of f will be taken into account, and more and more of g will be defined.

From 0 we derive

 (N i : i≥0 : f [i] ≤ f [x]) ≥ x+1 (2)
The weakest precondition that x := x+1 establishes
 (N i : i≥0 : f [i] ≤ y) ≥ x (3)
is, according to the axiom of assignment,
 (N i : i≥0 : f [i] ≤ y) ≥ x+1 ,

which, on account of (2), is implied by f [x] ≤ y; hence, the first alternative leaves (3), which is established by x, y := 0,0, invariant. So does the second alternative (obviously).

From f [x] > y we derive, on account of (0)

 (N i : i≥0 : f [i] ≤ y) ≤ x ,
which, in conjunction with (3) allows us to conclude that, then, (Ni : i≥0: f [i] ≤ y) = x. Hence, we have the second invariant
 (A j : 0≤j
and this is exactly the property I wanted to prove about my program

*              *
*

The example is — see EWD753— inspired by the theorem of Lambek and Moser, a theorem Wim Feijen found when looking for functions to be programmed in SASL. As a matter of fact, my “combined” program was not the first program I wrote to solve this problem: it is a direct translation of the following SASL definitions I wrote first: (my syntax)
 def k x y (p:q) = (5) if p ≤ y → k (x+1) y q ⫿ p > y → x : k x (y+1) (p:q) fi def g = k 0 0 f

But even the proof of the fact that g is ascending —which in the iterative program follows trivially from the equally obvious invariant

 y = 0 cor g[y−1] ≤ x —
was very painful when I tried a proof technique à la EWD749 which does justice to the “functional” nature of applicative languages: (5) is expressed in terms of tails, my proof is in terms of finite prefixes. I think I should ask an expert (See EWD759.)

 Plantaanstraat 5 9 November 1980 5671 AL NUENEN prof. dr. Edsger W. Dijkstra The Netherlands Burroughs Research Fellow

Transcribed by Martin P.M. van der Burgt
Last revision 10-Nov-2015 .