RTI uses cookies to offer you the best experience online. By clicking “accept” on this website, you opt in and you agree to the use of cookies. If you would like to know more about how RTI uses cookies and how to manage them please view our Privacy Policy here. You can “opt out” or change your mind by visiting: http://optout.aboutads.info/. Click “accept” to agree.
Proving loop termination: Beyond the traditional method
Chen, T., & Meyer, M. (2009). Proving loop termination: Beyond the traditional method. Journal of Computational Methods in Science and Engineering, 9(S2), 169-178. https://doi.org/10.3233/JCM-2009-0245
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.
