Proving loop termination: Beyond the traditional method

Article type: Research Article

Authors: Chen, Tennyson X.^{; *} | Meyer, Martin D.

Affiliations: Research Computing Division, RTI International 1, 3040 Cornwallis Road, Research Triangle Park, NC 27709, USA

Correspondence: [*] Corresponding author. Tel.: +919 990 8450; Fax: +919 541 6178; E-mail: [email protected].

Abstract: 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.

Keywords: Loop termination, iterative command, repetition construct, bound function, total correctness

DOI: 10.3233/JCM-2009-0245

Journal: Journal of Computational Methods in Sciences and Engineering, vol. 9, no. s2, pp. S169-S178, 2009