• Article

Proving loop termination: Beyond the traditional method

The traditional method for proving loop termination requires us to define a bound function of program variables. The criterion in this method is well-defined and can be easy to apply, as such functions are obvious for many loops. However in some cases, it can be very difficult to define a bound function. In this paper, we discuss how to prove loop termination by using alternative methods. First we show how to prove loop termination by solving a recursive relation that defines the number of iterations remaining in any execution state. Then we introduce a step-by-step approach for applying this recursive relation method. This new method can also be used to investigate preconditions that lead to loop termination in non-deterministic cases. Finally, we illustrate another method that uses a more general criterion for proving loop termination. The new criterion is a generalization of the classical one. This paper does not attempt to offer a one-size-fits-all approach. Rather, it provides some alternative methods that make proving loop termination easier in some cases, where termination might otherwise be difficult if not impossible to prove.

Citation

Chen, T., & Meyer, M. (2009). Proving loop termination: Beyond the traditional method. Journal of Computational Methods in Science and Engineering, 9(S2), 169-178. DOI: 10.3233/JCM-2009-0245

DOI Links