|
Termination Analysis through Combination of Type Based NormsMaurice Bruynooghe, Michael Codish, John Gallagher, Samir Genaim and Wim Vanhoof
ACM Transactions on Programming Languages and Systems;
29 (2): 10,
2007
Abstract:This paper makes two contributions to the work on semantics based termination analysis for logic programs. The first involves a novel notion of typebased norm where for a given type a corresponding norm is defined to count in a term the number of sub-terms of that type. This provides a collection of candidate norms, one for each type defined in the program. The second enables an analyser to base termination proofs on the combination of several different norms. This is useful when different norms are better suited to justify the termination of different parts of the program. Application of the two contributions together consists in considering the combination of the typebased candidate norms for a given program. This results in a powerful and practical technique. Both contributions have been introduced into a working termination analyser. Experimentation indicates that they yield state-of-the-art results in a fully automatic analysis tool, improving with respect to methods that do not use both types and combined norms.Available: bibtex entry postscript Related sites: Preliminary paper on combining norms from the ACM Portal Michael Codish The Department of Computer Science Ben-Gurion University of the Negev PoB 653, Beer-Sheva, 84105, Israel mcodish@cs.bgu.ac.il
|