A sequel to EWD592

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
	od

(The condition x ≥ 2 has been added to prevent the value sequence 0, 0, 0, ....; the condition x ≥ 3 has been added to prevent 1, 2, 1, 2, ... from occurring.)

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)

we don’t prove that directly, but construct a sequence of repetitive constructs

	DO_i: do B1_i → S1 ▯ ... ▯ Bj_i → Sj ▯ ... ▯ Bn_i ... Sn od	(3)
	for 1 = 0, 1, 2, ... such that P_i = wp(DO_i, R)	(4)

If for some value of ’i —or in the limit for i to infinity— we have P = P_i and DO = DO_i , then (2) has been proved.

With the abreviations for BB_i and P_i

BB_i = (E j: 1 ≤ j ≤ n: Bj_i) and P_i = BB_i or R

(5)

the method can be described as follows. Choose for i = 0 : BB₀ = F —i.e. all guards false— ; as a consequence we have P₀ = R . To perform the step from i to i+1 we choose for the Bj_i+1 solutions of the equations (1 ≤ j ≤ n):

(Bj_i ⇒ Bj_i+1) and (Bj_i+1 ⇒(Bj_i or (wp(Sj, P_i) and non P_i)))

(6)

If for a given value of i the only solution of (6) is Bj_i+1 = Bj_i for all j , then the game clearly stops; otherwise we choose for at least one value of j Bj_i+1 ≠ Bj_i . The result is that if P_i holds initially, DO_k for k ≥ i is certain to establish R in at most i steps. Formula (6) can be discovered by working backwards from the final state that should satisfy R; the last term ”and non P_i“ excludes that the weakening of Bj_i to Bj_i+1 introduces the possibility of nontermination.

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

The first program is deterministic, the second program is not, but the number of steps needed is a unique function of the initial value of x ; in the last program, the number of steps is not (always) uniquely determined by the initial value of x . I spent a few hours with Sintzoff’s method, and I think that they were well spent.

Plataanstraat 5 .	prof.dr.Edsger W.Dijkstra
NUENEN - 4565	Burroughs Research Fellow
The Netherlands

Transcribed by Martin P.M. van der Burgt
Last revision 2015-01-23 .