cTI

cTI: A Termination Inference EngineWelcome to the home page of the cTI system. cTI is the first bottomup lefttermination inference tool for ISOProlog. News
Termination InferenceWhen does a logic program terminate? Termination inference, a new kind of program analysis, answers this question with a compact formula, called a termination condition. All queries whose termination has been proven are described by this condition. For example, the conditionapp(A,B,C) terminates_if b(A);b(C)
is inferred for program app/3 .
Here, b(A) is true if the term size of A is bound,
i.e., if A is finite and ground.
Disjunctions are denoted as ; .
Thus, app/3 has been proven to terminate, if the first or the
last argument is bound.
Termination inference is an annotation free generalization of termination analysis/checking. It shifts the programmer's focus away from particular cases to the whole relation. Traditionally, a termination analyzer tries to prove that a given class of queries terminates. This class must be provided by the user, which is rather cumbersome if the programs have been written previously without any annotations. With termination inference no annotations are necessary. All provably terminating classes to all related predicates are inferred at once, illustrating the ``multidirectionality'' of predicates. This means that predicates can be used safely in several ``directions.'' cTI's ArchitecturecTI relies on two representations of the analyzed program: P_{N} and P_{B} In P_{N} all terms have been mapped to expressions in N (the set of natural numbers) according to a symbolic term size norm. The semantics of P_{N} is estimated and some control informations are inferred. P_{B} represents only the information whether an argument is bound, allowing to propagate boundedness information over the program.To determine the corresponding models, cTI makes heavy use of abstract interpretation techniques. The current implementation, written in SICStus Prolog, relies most notably on the Parma Polyhedra Library and the SICStus Prolog libraries CLP(Q) and CLP(B). For further details, please refer to the literature. The cTI SystemcTI (constraint based Termination Inference) infers classes of universally terminating programs for the leftmost selection rule (Prolog style execution). You can use cTI via the WWW, or immediately look at the benchmark collection. The TU Wien site also attempts to prove that the inferred conditions are optimal.cTI has been integrated into GUPU, a Prolog programming environment for beginners used at TU Wien and Université de La Réunion. cTI provides compact explanations for the (provable) properties of termination of all predicates and improves a slicingsystem in explaining reasons of nontermination. Sample ProgramsHere are some programs with which you can test cTI:
Contributors
Literature[Mesnard93] F. Mesnard, Etude de la terminaison des programmes logiques avec contraintes, au moyen d'approximations, PhD thesis, Université Paris VI, 1993. [Mesnard96] F. Mesnard, Inferring leftterminating classes of queries for constraint logic programs by means of approximations. In M. J. Maher, editor, Logic Programming: Proceedings of the Joint International Conference and Symposium on Logic Programming, MIT Press Series in Logic Programming, Bonn, Germany, 1996. The MIT Press. Pages 721. [NeumerkelM99] U. Neumerkel and F. Mesnard, Localizing and explaining reasons for nonterminating logic programs with failureslices. In G. Nadathur, editor, Principles and Practice of Declarative Programming, volume 1702 of Lecture Notes in Computer Science, Paris, France, 1999. SpringerVerlag, Berlin. Pages 328341. [MesnardN01] F. Mesnard and U. Neumerkel, Applying static analysis techniques for inferring termination conditions of logic programs. In P. Cousot, editor, Static Analysis: 8th International Symposium, SAS 2001, volume 2126 of Lecture Notes in Computer Science, Paris, France, 2001. Pages 93110. [MesnardPN02] F. Mesnard, E. Payet, and U. Neumerkel, Detecting optimal termination conditions of logic programs. In M. V. Hermenegildo and G. Puebla, editors, Static Analysis: 9th International Symposium, SAS 2002, volume 2477 of Lecture Notes in Computer Science, Madrid, Spain, 2002. SpringerVerlag, Berlin. Pages 509525. [MesnardR03] F. Mesnard and S. Ruggieri, On proving left termination of constraint logic programs. ACM Transactions on Computational Logic, 4(2):126, 2003. Related SystemsTermiLog: Termination analyzer by Naomi Lindenstrauss (here without frames). TerminWeb: Termination analyser by Michael Codish, Samir Genaim, and Cohavit Taboch. LPTP: A Logic Program Theorem Prover (proving left termination and other properties) by Robert Stärk. Ciao: Prolog development system with an upperbound complexity analyzer (upperbound complexity analysis encompasses termination analysis). Mercury contains a termination analyser (see the manual). TALP: Automatic termination proofs for wellmoded logic programs. [Page last updated on January 20, 2013, 16:47:51.] 


Home  Download 