
Proving Termination One Loop at a TimeMichael Codish and Samir Genaim
The 13th Workshop on Logic Programming Environments;
2003
Abstract:Classic techniques for proving termination require the identification of a measure that maps program states to the elements of a wellfounded domain. Termination is guaranteed if this measure is shown to decrease with each iteration of a loop in the program. This is a mph{global} termination condition  there exists a measure which is shown to decrease over all of the loops in the program. In recent years, systems based on mph{local} termination conditions are emerging. Here, termination is guaranteed if for every loop there exists a measure which decreases as execution follows through that loop. In this paper we question the relationship between the two approaches. Reasoning locally is more convenient. But is the local approach really more powerful? We show that for a large class of termination problems the two approaches are equally powerful. To this end we demonstrate that given local conditions which support a proof of termination, a corresponding global condition can always be constructed. On the one hand, the local conditions are simpler and easier to find. Yet on the other hand, in the local approach one must consider a closure operation on loops which may require to consider an exponential number of local conditions.Available: bibtex entry postscript Michael Codish The Department of Computer Science BenGurion University of the Negev PoB 653, BeerSheva, 84105, Israel mcodish@cs.bgu.ac.il
