Properties related to determinacy, failure, choice-points

Calls of the form X are deterministic, i.e., produce exactly one solution (or do not terminate).

Note that it can still leave choice points after its execution, but when backtracking into these, it can only fail or go into an infinite loop.

These properties are inferred and checked natively by CiaoPP using the domains and techniques of [LGBH05,LGBH10,DLGH97,BLGH04].

Usage:det(X)

Calls of the form X are deterministic.

Calls of the form X are semi-deterministic, i.e., produce at most one solution (or do not terminate).

Note that it can still leave choice points after its execution, but when backtracking into these, it can only fail or go into an infinite loop.

These properties are inferred and checked natively by CiaoPP using the domains and techniques of [LGBH05,LGBH10,DLGH97,BLGH04].

Usage:semidet(X)

Calls of the form X are semi-deterministic.

Calls of the form X are multi-deterministic, i.e., they produce one or more solutions and do not fail.

Usage:multi(X)

Calls of the form X are multi-deterministic.

Nothing is ensured about failure and determinacy of calls to X. This is the default when no information is given for a predicate, so this property does not need to be stated explicitly.

Usage:nondet(X)

Calls of the form X are non-deterministic.

• The following properties should hold globally:
  (basic_props:no_rtcheck/1)nondet(X) is not checked during run-time checking.

For any call of the form X there is at most one clause whose test (guard) succeeds, i.e., clause tests are pairwise exclusive. Note that determinacy is the transitive closure (to all called predicates) of this property. This property is inferred and checked natively by CiaoPP using the domains and techniques of [LGBH05,LGBH10].

Usage:mut_exclusive(X)

For any call of the form X at most one clause test succeeds.

• The following properties should hold globally:
  (basic_props:rtcheck/2)The runtime check of this property is unimplemented.

For calls of the form X more than one clause test may succeed. I.e., clause tests are not disjoint for some call.

Usage:not_mut_exclusive(X)

For some calls of the form X more than one clause test may succeed.

• The following properties should hold globally:
  (basic_props:rtcheck/2)The runtime check of this property is unimplemented.

Mutual exclusion of the clause tests for calls of the form X cannot be ensured. This is the default when no information is given for a predicate, so this property does not need to be stated explicitly.

Usage:possibly_not_mut_exclusive(X)

Mutual exclusion is not ensured for calls of the form X.

• The following properties should hold globally:
  (basic_props:no_rtcheck/1)possibly_not_mut_exclusive(X) is not checked during run-time checking.

For any call of the form X there is at least one clause whose test (guard) succeeds (i.e., all the calls of the form X are covered). Note that nonfailure is the transitive closure (to all called predicates) of this property. [DLGH97,BLGH04].

Usage:covered(X)

All the calls of the form X are covered.

• The following properties should hold globally:
  (basic_props:rtcheck/2)The runtime check of this property is unimplemented.

There is some call of the form X for which there is no clause whose test succeeds [DLGH97].

Usage:not_covered(X)

Not all of the calls of the form X are covered.

• The following properties should hold globally:
  (basic_props:rtcheck/2)The runtime check of this property is unimplemented.

Covering is not ensured for any call of the form X. In other words, nothing can be ensured about covering of such calls.

Usage:possibly_not_covered(X)

Covering is not ensured for calls of the form X.

• The following properties should hold globally:
  (basic_props:no_rtcheck/1)possibly_not_covered(X) is not checked during run-time checking.

Usage:no_choicepoints(X)

A call to X does not leave new choicepoints.

Usage:leaves_choicepoints(X)

A call to X leaves new choicepoints.

All calls of the form X are deterministic, i.e., produce at most one solution (or do not terminate). In other words, if X succeeds, it can only succeed once. It can still leave choice points after its execution, but when backtracking into these, it can only fail or go into an infinite loop. This property is inferred and checked natively by CiaoPP using the domains and techniques of [LGBH05,LGBH10].

Usage:is_det(X)

All calls of the form X are deterministic.

All calls of the form X are non-deterministic, i.e., they always produce more than one solution.

Usage:non_det(X)

All calls of the form X are non-deterministic.

Non-determinism is not ensured for calls of the form X. In other words, nothing can be ensured about determinacy of such calls. This is the default when no information is given for a predicate, so this property does not need to be stated explicitly.

Usage:possibly_nondet(X)

Non-determinism is not ensured for calls of the form X.

• The following properties should hold globally:
  (basic_props:no_rtcheck/1)possibly_nondet(X) is not checked during run-time checking.

Calls of the form X produce at least one solution (succeed), or do not terminate. This property is inferred and checked natively by CiaoPP using the domains and techniques of [DLGH97,BLGH04].

Usage:not_fails(X)

All the calls of the form X do not fail.

• The following properties should hold globally:
  (basic_props:native/1)This predicate is understood natively by CiaoPP.

Non-failure is not ensured for any call of the form X. In other words, nothing can be ensured about non-failure nor termination of such calls.

Usage:possibly_fails(X)

Non-failure is not ensured for calls of the form X.

• The following properties should hold globally:
  (basic_props:no_rtcheck/1)possibly_fails(X) is not checked during run-time checking.