An intriguing example

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, (N i : i≥0: f [i] ≤ y) = x. Hence, we have the second invariant

(A j : 0≤j<y : g[j] = (N i : i≥0 : f [i] ≤ j))

(4)

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 .