 |
One Loop at a Time
Michael Codish, Samir Genaim, Maurice Bruynooghe, John Gallagher and Wim Vanhoof
6th International Workshop on Termination (WST 2003);
2003
Abstract:
Classic techniques for proving termination require the identification of a measure mapping program states to the elements of a well founded domain and to show that this measure decreases with each iteration of a loop in the program. This is a global termination condition --- there is a single measure which must be shown to decrease over all of the loops in the program. In this note we look at systems based on local termination conditions which allow the involvement of different well founded domains and termination measures for different loops in the program. We illustrate the practical advantages of applying local criteria in automated termination proving systems and demonstrate how Ramsey Theorem clarifies their formal justification.Available: bibtex entry postscript
Michael Codish
The Department of Computer Science
Ben-Gurion University of the Negev
PoB 653, Beer-Sheva, 84105, Israel
mcodish@cs.bgu.ac.il