Reuse of Results in Termination Analysis of Typed Logic Programs
Proceedings of The 9th International Static Analysis
Symposium (SAS 2002 - to appear);
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
The Department of Computer Science
Ben-Gurion University of the Negev
PoB 653, Beer-Sheva, 84105, Israel