Loop Termination
To show that a loop terminates we introduce an integer function, t. where t is a function of the program variables i.e. an upper bound on the number of iterations still to be performed.
t is called the variant function and it is a measure of the amount of work yet to be completed by the loop.
Each iteration of the loop decreases t by at least one
As long as execution of the loop has not terminated then t is bounded below by 0. Hence the loop must terminate.
In our last example t: 11-i