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 :
• Relations on pairs of argument positions : size dependencies are of the form :
`X=Y,X<Y,X=<Y`
for pairs of argument positions.
• Polyhedra : size dependencies are given in a form of polyhedra : general linear dependencies between 2 or more argument positions.
Selecting either method you can get different results from the analysis.

• 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 :
defsize(Pattern, Size).

Where :
• 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.
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 non-variable terms".

For example the list-length norm can be defined as follows :

```[defsize([X|Xs],1+size(Xs)),
defsize([],0),
defsize(X,0)].
```

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 prove termination.