Using The System
Goal Independent Stage
In the main system page you should enter a prolog file name to be analyzed.
You can optionally change the following parameters :
- Symbolic norm :
- Term size - which counts the number of edges in the term-tree.
- List size - which measures the length of a list.
- Define other symbolic norm.
- Computing bottom up size dependencies :
Selecting either method you can get different results from the analysis.
- Relations on pairs of argument positions : size dependencies are of the form :
for pairs of argument positions.
- Polyhedra : size dependencies are given in a form of polyhedra : general
linear dependencies between 2 or more argument positions.
- Number of steps before widening : The polyhedra domain requires using
widening. The widening is performed after computing N facts (2,3, or 4)
according to the selected value.
Using a larger value is more accurate, but also slower.
- Computing binary unfoldings :
- Goal dependent : the closure of binary unfoldings is computed after
the initial goal is given and only for the relevant calls.
- Goal independent : the closure of binary unfoldings is computed
in the first stage. The result is that the goal independent stage
is longer and the goal dependent stage is very fast. It is better to
use this option if you want to check several initial goals for one program.
Defining Other Symbolic Norms
This can be done by entering the specifications of the desired norm
in the text box.
Specifying a norm is done by using the predicate defsize/2 :
If there is a pattern in the program which there is no norm specified
then the term size norm will be applied.
The symbolic norm of a variable is always the variable itself.
For this reason, a variable in the pattern argument means : "For all other
- Pattern is the pattern of the term the norm should be defined for.
It should be of the form f(X1,X2,...,Xn) where f is a function symbol
and X1,X2,...,Xn are distinct variables.
- Size is the way the norm should be computed. This expression
should be of the form : "T1 + T2 + ..." where each Ti is either
a natural number, or a term of the form size(X) and X is one of the
variables in the given pattern.
For example the list-length norm can be defined as follows :
Goal Dependent Stage
In the goal dependent stage you should enter an initial abstract goal.
The abstraction is done by replacing the concrete arguments of the predicate
by the abstract terms 'b' and 'f' which stand for bound and free arguments
according to the chosen symbolic norm.
(For example, an argument position is bound w.r.t term size if it is ground.
If using the list length norm, 'b' indicates that the argument is a closed list).
The abstract query should be terminated with a dot.
The results of analyzing the query are :
- An answer if the query terminates or possibly no.
- A description (in the abstract domains of instantiation and size dependencies)
of all possible calls and the matching binary clauses.
- A graphic representation of the recursive binary clauses
with the matching calls. (If requested by the user).
- Some of the clauses show the decrease in an instantiated argument position
in a red arrow.
- If all the binary clauses contain an argument position which is
instantiated and its size strictly decreases, then the query terminates.
Otherwise the clauses that do not contain this red arrow are the cause for
a possible non-termination, or for the inability of the system to