cTI: a constraint-based Termination Inference tool for ISO-Prolog


Introduction:
-------------

cTI is an automatic tool for inferring universal left termination conditions
of any ISO-Prolog programs. In other words, given a Prolog program,
cTI tries to compute all the modes for all user-defined predicates
which insures that the Prolog processor will give all answers in finite time.
NB : cTI assumes that no infinite rational term is created at run-time 
while running the analyzed program.


Requirements:
-------------

SWI-Prolog >= 8


Installing and running cTI:
---------------------------

The file cTI is a Prolog script which compiles the analyzer on the fly
and analyzes the file passed as an argument. For instance, inside the src/ directory, 
any Prolog source can be analyzed from the terminal. Consider the Prolog program in Filex/testapp3.pl:

	% app3(Xs, Ys, Zs, Us) iff Us is the result of concatentating the lists Xs, Ys and Zs
	app3(Xs,Ys,Zs,Us) :- app(Xs,Ys,Vs), app(Vs,Zs,Us).

	% idem but note that the atoms in the body have been swapped
	app3bis(Xs,Ys,Zs,Us) :- app(Vs,Zs,Us), app(Xs,Ys,Vs).

	% app(Xs,Ys,Zs) iff Zs is the concatenation of Xs and Ys 
	app([],Ys,Ys).
	app([X|Xs],Ys,[X|Zs]) :- app(Xs,Ys,Zs).
	
	% rev(Xs,Ys) iff Ys is Xs in the reverse order
	rev([],[]).
	rev([X|Xs],Zs) :- rev(Xs,Ys), app(Ys,[X],Zs).

Let us ask for its terminating modes:

	% ./cTI Filex/testapp3.pl    
	...
	predicate_term_condition(rev(A,B),A).
	predicate_term_condition(app(A,B,C),C+A).
	predicate_term_condition(app3(A,B,C,D),A*D+A*B).
	predicate_term_condition(app3bis(A,B,C,D),D).

which means that, wrt the Prolog program Filex/testapp3.pl:
- rev/2 terminates if its first argument is ground,
- app/3 terminates if its first or third argument is ground,
- app3/4 terminates if either its first and fourth arguments are ground
  or its first and second argument are ground,
- app3bis terminates if its fourth argument is ground.


Options:
--------

- Unknown predicates are assumed to finitely failed, which is the
standard behavior of any ISO-Prolog conforming system.
It is possible to get compatibility with most Prolog dialects
by adding at the beginning of the file:
	:- include_predef('predef_for_compatibility.pl').
By modifying the file predef_for_compatibility.pl,
the user may define its own set of built-ins.

- cTI includes a TERMCOMP mode. If the analyzed Prolog source contains a line:
%query: <pred>(<i|o|b|f|g|a>*).
then cTI will check whether the corresponding set of queries
terminates and answers YES or MAYBE, e.g.:
If we add the line
%query: app3(i,i,o,o).
to the file Filex/testapp3.pl resulting in the file Filex/testapp3TC.pl,
we get:
	   $ ./cTI Filex/testapp3TC.pl 
	   YES
It means that app3/4 terminates if its first and second argument are ground.


Acknowledgements:
-----------------

Fred Mesnard designed and implemented the analyzer in the 90's.
cTI was publicly announced on comp.lang.prolog the 22th of April 2000.
The first version was written in SICStus Prolog. 
Ulrich Neumerkel helped while debugging the analyzer. 
Roberto Bagnara wrote the interface between cTI and the PPL, which is not needed for this version. 
Markus Triska wrote a SWI-Prolog version of the SICStus CLP(B) solver which enabled the port of cTI to SWI-Prolog. 
Finally, thanks to Markus Triska and Etienne Payet for triggering this port.



------------------------------------------------------------------------
Copyright (C) 2000-... Fred Mesnard -- frederic.mesnard@univ-reunion.fr
------------------------------------------------------------------------