NOTE: This transcription was contributed by Martin P.M. van der Burgt, who has devised a process for producing transcripts automatically. Although its markup is incomplete, we believe it serves a useful purpose by virtue of its searchability and its accessibility to text-reading software. It will be replaced by a fully marked-up version when time permits. —HR
5th January 1977
A sequel to EWD592.
Recently I lectured on the structure of proofs for termination in Munich. Lack of time had prevented me from giving the argument why a variant function that decreases monotonically, must exist, and the next morning miss dr. Mila Majster, who had been in my audience, presented to me what she felt could be a counterexample. Her example was essentially:
|do odd (x)and x ≥ 3 → x:= x + 1|
|▯ even(x)and x ≥ 2 → x:= x / 2|
My first guess at a single t was wrong. I have posed the problem to a number of my Dutch colleagues, and all first proposals were wrong. After my failure I decided to apply the technique of EWD592m writing t = t1 + t2 such that t1 is decreaed by the first alternative and left invariant by the second, and for t2 the other way round. My construction was ingenious —so ingenious that I showed it proudly to a number of people!— but in St.Pierre de Chartreuse .... I discovered that it was wrong!
A next time I proceeded more carefully. Because I had the feeling that the binary representation of x could provide a good handle and the second alternative is in terms of the bits the simplest, I first looked for t2 .
Well the quantity that is obviously decreased by 1 by x:= x / 2 is the number of trailing zero’s or, alternatively, the number of significant digits. As first approxiamtion I took the latter; because it depends on the position of the most-significant 1 , it has the advantage of being undefined for x = 0, thereby justifying the constraint x ≥ 2 . The problem is that the first alternative increases it by 1 if x:= x + 1 forms a power of 2. Because being a power of 2 is invariant under x:= x / 2 , a good proposal is t2 = the number of significant digits of x , decreased by 1 iff x is a power of 2 .
Searching for a t1 took me more time. Because t1 must be invariant under x:= x / 2 , it should be a function of the digit pattern as it extends itself from the most- to the least-significant 1 in x . Because adding 1 will turn a number of trainling 1’s into 0’s and then a 0 into a 1, my first guess was something like the number of “internal zero” (i.e. between the most and the least-significant 1’s). I then realized, that the number of internal zero’s fails to be decreased by 1 if by x:= x + 1 a power of 2 is formed. Hence I concocted
t1 = the number of internal 0’s of x , increased by 1 iff x is not a power of 2 .
This t1 has the advantage of excluding x = 1, hence the condition x ≥ 3 .
Adding t1 + t2 I derived:
t = 1 + the number of significant digits + the number of internal 0’s, decreased by 2 iff x is a power of 2 .
|x (in binary)||t(x)|
|10||1 + 2 + 0 - 2 = 1|
|11||1 + 2 + 0 = 3|
|100||1 + 3 + 0 - 2 = 2|
|101||1 + 3 + 1 = 5|
|110||1 + 3 + 0 = 4|
|111||1 + 3 + 0 = 4|
|1000||1 + 4 + 0 - 2 = 3|
|1001||1 + 4 + 2 = 7 etc.|
The best thing that can be said for my t is that t1 is exactly the number of times the first alternative will be chosen, and t2 is exactly the number of times the second alternative will be chosen: it gives you all the timing information. But if we are only interested in termination, the amount of work we have spent seems excessive, and there is clearly room for techniques of proving the existence of a variant function without actually constructing one.
In St.Pierre de Chartreuse M.Sintzoff showed me another way of proving the termination of repetitive constructs. As yet I have no feeling for the significance of his method, but it intruged me enough to try to reconstruct what he had shown me, and I think that in any case the method deserves to be recorded. In order to prove for a given repetitive construct
|DO: do B1 → S1 ▯ ... ▯ Bj → Sj ▯ ... ▯ Bn ... Sn od||(1)|
|we have for a certain P and R P = wp(DO, R)||(2)|
|DOi: do B1i → S1 ▯ ... ▯ Bji → Sj ▯ ... ▯ Bni ... Sn od||(3)|
|for 1 = 0, 1, 2, ... such that Pi = wp(DOi, R)||(4)|
With the abreviations for BBi and Pi
|BBi = (E j: 1 ≤ j ≤ n: Bji) and Pi = BBi or R||(5)|
|(Bji ⇒ Bji+1) and (Bji+1 ⇒(Bji or (wp(Sj, Pi) and non Pi)))||(6)|
The charm of Sintzoff’s method is that it is so constructive. With S1: x:= x + 1 , S2: x:= x - 1 , S3: x:= x - 2 we derived with R: x = 0 and P: x ≥ 0 without problems the following programs
|do false → x:= x + 1 ▯ x = l → x:= x - 1 ▯ x ≥ 2 → x:= x - 2 od|
|do false → x:= x + l ▯ podd(x) → x:= x - l ▯ x ≥ 2 → x:= x - 2 od|
|do podd(x) → x:= x + l ▯ podd(x) → x:= x - l ▯ peven(x) → x:= x - 2 od|
|Plataanstraat 5 .||prof.dr.Edsger W.Dijkstra|
|NUENEN - 4565||Burroughs Research Fellow|
Transcribed by Martin P.M. van der Burgt