|
Reuse of Results in Termination Analysis of Typed Logic ProgramsMaurice Bruynooghe, Michael Codish, Samir Genaim and Wim Vanhoof
Proceedings of The 9th International Static Analysis
Symposium (SAS 2002 - to appear);
2002
Abstract:Recent works by the authors address the problem of automating the selection of a candidate norm for the purpose of termination analysis. These works illustrate a powerful technique in which a collection of simple type-based norms --- one for each data type in the program --- are combined together to provide the candidate norm. The current paper extends these results by investigating type polymorphism. We show that by considering polymorphic types we reduce, without sacrificing precision, the number of type-based norms which should be combined to provide the candidate norm. Moreover, we show that when a generic polymorphic typed program component occurs in one or more specific type contexts, we need not reanalyse it. All of the information concerning its termination and its effect on the termination of other predicates in that context can be derived directly from the context independent analysis of that component based on norms derived from the polymorphic types.Available: bibtex entry Related sites: Michael Codish The Department of Computer Science Ben-Gurion University of the Negev PoB 653, Beer-Sheva, 84105, Israel mcodish@cs.bgu.ac.il
|