Alternative Methods in Proving Loop Termination

摘要

The usual formal criterion for establishing termination of a loop requires that the programmer define an integer function t (a "bound function") of program variables whose value is bounded below by 1, as long as termination has not occurred, and whose value decreases by at least 1 on each loop iteration. This method is defined in [1], [2], [4], [5], [6], [7], as well as in other literature in the field of formal methods. While the criterion in this well-defined method is often rather straightforward to apply, it is sometimes very difficult to define the bound function, even though, at least for the deterministic case, such a function always exists for a terminating loop. A recent attempt in [8] to prove loop termination without using a bound function still leaves some cases very difficult to solve.rnIn this paper, we will discuss how to prove loop termination by using alternative methods. First we will show how to prove loop termination by solving a recursive relation that defines the number of iterations remaining in any execution state. Then we will illustrate a more general criterion that can be used for proving loop termination. The new criterion is a generalization of the classical one. This paper does not intend to offer a one-size-fits-all approach. Instead, it provides some alternative methods that make proving loop termination easier in some cases which might otherwise be difficult if not impossible to prove.