app(A,B,C) terminates_if b(A);b(C)is inferred for program
b(A)is true if the term size of
Ais bound, e.g. finite and ground. Disjunctions are denoted as
app/3has 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 `multi-directionality' of predicates. This means that predicates can be used safely in several `directions'.
cTI_lt has been integrated into GUPU, a Prolog programming environment for beginners used at TU Wien and Univ. de La Réunion. cTI_lt explains compactly the (provable) properties of termination of all predicates and improves a slicing-system in explaining reasons of nontermination.
To determine the corresponding models, cTI uses heavily abstract interpretations. The current implementation uses SICStus Prolog relying most notably on its libraries CLP(Q) (to perform calculations in N) and CLP(B). For further details, please refer to the literature.
[Mes96] F. Mesnard, Inferring left-terminating classes of queries for constraint logic programs. JICSLP'96, 7-21, MIT Press, 1996.
[HoaMes98] S. Hoarau and F. Mesnard, Inferring and Compiling Termination for Constraint Logic Programs. LOPSTR 1998, 240-254, LNCS 1559, Springer-Verlag, 1999.
[NeuMes99] U. Neumerkel and F. Mesnard, Localizing and explaining reasons for nonterminating logic programs with failure slices. PPDP'99, 328-341, LNCS 1702, Springer-Verlag, 1999.
[MesNeu01] F. Mesnard and U. Neumerkel, Applying static analysis techniques for inferring termination conditions of logic programs. SAS'01, 93-110, LNCS 2126, Springer-Verlag, 2001.
[MesPayNeu02] F. Mesnard, E. Payet, and U. Neumerkel, Detecting Optimal Termination Conditions of Logic Programs. SAS'02, 509-525, LNCS 2477, Springer-Verlag 2002.
TermiLog (without frames). Termination analyzer by Naomi Lindenstrauss.
TerminWeb. Termination analyser by Michael Codish and Cohavit Taboch.
TALP. Automatic termination proofs for well-moded logic programs.
LPTP. Logic program theorem prover (proving left termination and other properties) by Robert Stärk.
Ciao. Prolog development system with an upper-bound complexity analyzer. If the property steps_ub/2 with a finite upper-bound has been proven, also termination has been proven. Upper-bound analysis therefore generalizes termination analysis in another direction.
Mercury contains a termination analyser (Manual).
Hasta-La-Vista. Termination analyser for logic programs equipped with numerical computations.