Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
cTI: A Constraint-Based Termination Inference Tool for ISO-Prolog

cTI: A Constraint-Based Termination Inference Tool for ISO-Prolog

Fred Mesnard
IREMIA
Université de La Réeunion
15, Avenue René Cassin - BP 7151
97715 Saint Denis
La Réunion
France

Roberto Bagnara
Dipartimento di Matematica
Università di Parma
Viale G. P. Usberti 53/A
I-43100 Parma
Italy

Abstract:

We present cTI, the first system for universal left-termination inference of logic programs. Termination inference generalizes termination analysis and checking. Traditionally, a termination analyzer tries to prove that a given class of queries terminates. This class must be provided to the system, for instance by means of user annotations. Moreover, the analysis must be redone every time the class of queries of interest is updated. Termination inference, in contrast, requires neither user annotations nor recomputation. In this approach, terminating classes for all predicates are inferred at once. We describe the architecture of cTI and report an extensive experimental evaluation of the system covering many classical examples from the logic programming termination literature and several Prolog programs of respectable size and complexity.

Keywords: Termination Inference; Termination Analysis; Logic Programming; Abstract Interpretation.

Available: PDF, 300 DPI, 600 DPI, and 1200 DPI PostScript, DVI, BibTeX entry.

[Page last updated on May 03, 2004, 12:55:51.]