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
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
.