SPIDER Determinacy Analyzer

SPIDER automatically analyzes determinacy and nondeterminacy of predicates. The inferred information can be presented as problem or information markers and is shown in the info-pop documentation of predicates.

The functionality is similar in spirit to, but not the same as, the one provided by the spdet tool and the Determinacy Checker library.

The determinacy analyzer in SPIDER can help you spot unwanted nondeterminacy in your programs. SPIDER examines your program source code and points out places where nondeterminacy may arise. It is not in general possible to find exactly which parts of a program will be nondeterminate (or determinate) without actually running the program. However, SPIDER can find some, and perhaps most, unwanted nondeterminacy.

Unintended nondeterminacy should be eradicated because:

It may give you wrong answers on backtracking.
It may cause a lot of memory to be wasted

In addition, the nondeterminacy that SPIDER detects may indicate a typo or other bug in the code.

Declaring Nondeterminacy

Some predicates are intended to be nondeterminate. By declaring intended nondeterminacy, you avoid warnings about predicates you intend to be nondeterminate. Equally important, you also inform the determinacy analyzer about nondeterminate predicates. It uses this information to identify unwanted nondeterminacy. Nondeterminacy is declared by putting a declaration of the form

     :- name/arity is nondet.

in your source file. This is similar to a dynamic or discontiguous declaration.

Similarly, a predicate P/N may be classified as nondeterminate by the analyzer, whereas in reality it is determinate. This may happen e.g. if P/N calls a dynamic predicate that in reality never has more than one (determinate) clause. To prevent false alarms arising from this, you can inform the analyzer about determinate predicates by declarations of the form:

     :- name/arity is semidet.

Using is/2 as a directive in this way is supported natively in SICStus Prolog 4.2.1. For older versions of SICStus you can wrap the directive in a conditional so that only SPIDER sees it, something like:

     :- if current_prolog_flag(dialect, spider).
     :- name/arity is semidet.
     :- endif. % SPIDER

A complete example would look like:

% parent.pl (this code requires SICStus Prolog 4.2.1)
:- module(parent, [parent/2, is_parent/1]).

:- parent/2 is nondet.
parent(abe, rob).
parent(abe, sam).
parent(betty, rob).
parent(betty, sam).

:- is_parent/1 is nondet.
is_parent(Parent) :-
        parent(Parent, _).

An alternative, older, syntax is also available, see below.

What is Detected

It is not in general possible to find exactly which places in a program will lead to nondeterminacy. The determinacy analyzer gives predicates the benefit of the doubt: when it's possible that a predicate will be determinate, it will be assumed determinate. The analyzer will only report as nondeterminate places in your program that will be nondeterminate regardless of which arguments are bound.

The determinacy analyzer looks for the following sources of nondeterminacy:

Multiple clauses of that can't be distinguished by the principal functor of the first arguments, and are not made determinate with an explicit cut (!), or by not succeeding (e.g. by calling fail/0 or throw/1).
Predicates where not all clauses are available for analysis, i.e. undefined predicates, dynamic predicates and multifile predicates.
Disjunctions where more than one branch may succeed without performing a cut, and the disjunction is followed by code that may succeed without performing a cut.
A clause that calls something inferred, or declared, to be nondeterminate when the call is is followed by code that may succeed without performing a cut.
Calls to builtins and library predicates known to be possibly nondeterminate.

The above description is a simplification. In addition, the analyzer uses special knowledge about many builtins and library predicates and of the SICStus Prolog compiler in order to increase the accuracy of the inferred information.

Analyzer Result

The result of the analysis is used in two ways:

It is presented in the info-pop documentation shown by SPIDER when the mouse pointer hover over a predicate name. (This is not done for documented library predicates. The assumption is that determinacy information is present in the library documentation.)
As problem/warning/information markers in the left margin of the editor. By default the only presented information is when a predicate has been determined nondeterminate and when a predicate has been determined to not succeed (i.e. fail, throw or loop). The severity of these problem markers can be increased and other inferred information can be presented by changing their preferences in the Errors/Warnings preference pane.

Integration with older versions of SICStus Prolog

Note: You can ignore this section if you use SICStus Prolog 4.2.1 or newer. SICStus Prolog 4.2.0 and older, and the accompanying determinacy checker tool, did not support the use of is/2 as a directive. Instead you would use a pseud-directive det/1 and nondet/1 to declare a predicate as determinate and non-determinate, respectively, as follows:

     % Older syntax, requires det/1 to be defined.
     :- det name/arity. % corresponds to: name/arity is semidet.
     :- nondet name/arity. % corresponds to: name/arity is nondet.

By default SICStus Prolog does not recognize the nondet/1 and det/1 directives. Instead they will be treated as calls to undefined predicates and lead to errors during loading of the program and warnings in SPIDER.

One way to solve this is to define nondet/1 and det/1 as predicates that does nothing. This is what library(nondetdecl) does and it also defines nondet and det as prefix operators, similar to directives like mode/1. A downside to this method is that the calls will still be performed when your code is loaded. It may therefore be preferable to wrap the code with a conditional directive that ensures that only SPIDER sees the determinacy declarations (but in that case you may as well use the new is/2 directives).

So, to make a long story short, to use the old syntax, do this after you have declared your module:

     :- if(current_prolog_flag(dialect, spider)).
     :- ensure_loaded(library(nondetdecl)).
     :- endif.

and, when you want to declare the determinacy of some predicate you wrap that too in a conditional directive, so a complete example would look like:

% parent.pl (this code works in any version of SICStus Prolog)
:- module(parent, [parent/2, is_parent/1]).

:- if(current_prolog_flag(dialect, spider)).
:- use_module(library(nondetdecl)).
:- endif.

:- if(current_prolog_flag(dialect, spider)).
:- nondet parent/2.
:- nondet is_parent/1.
:- endif.
     
parent(abe, rob).
parent(abe, sam).
parent(betty, rob).
parent(betty, sam).

is_parent(Parent) :-
        parent(Parent, _).

By using conditional compilation only SPIDER sees the determinacy directives, thus ensuring that there are no costs when the code is compiled or loaded in SICStus Prolog.

Note: The documentation for library(nondetdecl) and library(detcheck) claims that you only need to load them at compile time (using the when(compile_time) option to load_files/2). Unfortunately there is a bug in current versions of those libraries which makes it necessary for the libraries to be loaded also at load time. We expect that this will be fixed in a future version of SICStus Prolog. Using the is/2 directive or the SPIDER-only conditional compilation, as above, works around this bug.

Send feedback on SPIDER.

Last modified: Mon Sep 5 20:14:14 CEST 2011