CMP.13:5.2 - Obtain a loop property without enumerating its iterations

Consider unbounded integers, positive integer N, and:

x = 0
while x < N:
    x = x + 1

At the loop head, a set X of possible values is transformed by F(X)={0} ∪ {x+1: x∈X and x<N}. An interval hull supplies an abstract transformer. Starting at [0,0] produces [0,1], [0,2] and so on until [0,N]; this takes a number of expansions proportional to N even though N can be written with logarithmically many bits.

Widen the increasing upper endpoint of [0,0] and [0,1] to obtain [0,+infinity]. It contains the initial value and is closed under the guarded update. It already establishes that x is never negative.

Suppose the receiving question instead asks for the value on exit. Apply the guard to [0,+infinity]: the integer inputs admitted by x<N are [0,N-1]; adding one and joining the initial value gives [0,N]. This smaller interval is itself closed under F, and contains 0. The exit condition x>=N then leaves [N,N]. Therefore every terminating execution exits with x=N.

For a termination conclusion, add a different argument: while the guard holds, the nonnegative integer N-x decreases by one, and the arithmetic is unbounded. This proves termination from 0 for the stated positive N. It explains why the exit value is obtained, rather than merely describing it if obtained.

Changed condition: replace the update by x=x+2, retaining N=5. The guarded interval calculation now gives [0,6]; exit intersection gives [5,6]. If that bound is sufficient, stop. If the final value is needed, retain the invariant that x is even as well. The exit result becomes {6}. The old answer 5 was tied to the former update.