Properties which are native to analyzers

Author(s): Francisco Bueno, Manuel Hermenegildo, Pedro Lopez.

Version: 1.10#7 (2006/4/26, 19:22:13 CEST)

Version of last change: 1.9#86 (2003/7/17, 16:59:29 CEST)

This library contains a set of properties which are natively understood by the different program analyzers of ciaopp. They are used by ciaopp on output and they can also be used as properties in assertions.

• Usage and interface (native_props)
• Documentation on exports (native_props)

Usage and interface (native_props)

Documentation on exports (native_props)

PROPERTY: covered/2:

covered(X, Y)

All variables occuring in X occur also in Y.

Usage: covered(X, Y)

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

PROPERTY: linear/1:

linear(X)

X is bound to a term which is linear, i.e., if it contains any variables, such variables appear only once in the term. For example, [1,2,3] and f(A,B) are linear terms, while f(A,A) is not.

Usage: linear(X)

• Description: X is instantiated to a linear term.
• The following properties hold globally: This predicate is understood natively by CiaoPP. (basic_props:native/1)

PROPERTY: mshare/1:

mshare(X)

X contains all sharing sets [JL88,MH89] which specify the possible variable occurrences in the terms to which the variables involved in the clause may be bound. Sharing sets are a compact way of representing groundness of variables and dependencies between variables. This representation is however generally difficult to read for humans. For this reason, this information is often translated to ground/1, indep/1 and indep/2 properties, which are easier to read.

Usage: mshare(X)

• Description: The sharing pattern is X.
• The following properties should hold globally: This predicate is understood natively by CiaoPP as sharing(X). (basic_props:native/2)

PROPERTY: nonground/1:

Usage: nonground(X)

• Description: X is not ground.
• The following properties should hold globally: This predicate is understood natively by CiaoPP as not_ground(X). (basic_props:native/2)

PROPERTY: fails/1:

fails(X)

Calls of the form X fail.

Usage: fails(X)

• Description: Calls of the form X fail.
• The following properties hold globally: This predicate is understood natively by CiaoPP. (basic_props:native/1)

PROPERTY: not_fails/1:

not_fails(X)

Calls of the form X produce at least one solution, or not terminate [DLGH97].

Usage: not_fails(X)

• Description: All the calls of the form X do not fail.
• The following properties hold globally: This predicate is understood natively by CiaoPP. (basic_props:native/1)

PROPERTY: possibly_fails/1:

possibly_fails(X)

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

Usage: possibly_fails(X)

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

PROPERTY: covered/1:

covered(X)

For any call of the form X there is at least one clause whose test succeeds (i.e. all the calls of the form X are covered.) [DLGH97].

Usage: covered(X)

• Description: All the calls of the form X are covered.

PROPERTY: not_covered/1:

not_covered(X)

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

Usage: not_covered(X)

• Description: Not all of the calls of the form X are covered.

PROPERTY: is_det/1:

is_det(X)

All calls of the form X are deterministic, i.e. produce at most one solution, or not terminate.

Usage: is_det(X)

• Description: All calls of the form X are deterministic.

PROPERTY: non_det/1:

non_det(X)

All calls of the form X are not deterministic, i.e., produce several solutions.

Usage: non_det(X)

• Description: All calls of the form X are not deterministic.

PROPERTY: possibly_nondet/1:

possibly_nondet(X)

Non-determinism is not ensured for all calls of the form X. In other words, nothing can be ensured about determinacy nor termination of such calls.

Usage: possibly_nondet(X)

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

PROPERTY: mut_exclusive/1:

mut_exclusive(X)

For any call of the form X at most one clause succeeds, i.e. clauses are pairwise exclusive.

Usage: mut_exclusive(X)

• Description: For any call of the form X at most one clause succeeds.

PROPERTY: not_mut_exclusive/1:

not_mut_exclusive(X)

Not for all calls of the form X at most one clause succeeds. I.e. clauses are not disjoint for some call.

Usage: not_mut_exclusive(X)

• Description: Not for all calls of the form X at most one clause succeeds.

PROPERTY: size_lb/2:

size_lb(X, Y)

The minimum size of the terms to which the argument Y is bound to is given by the expression Y. Various measures can be used to determine the size of an argument, e.g., list-length, term-size, term-depth, integer-value, etc. [DL93].

Usage: size_lb(X, Y)

• Description: Y is a lower bound on the size of argument X.

PROPERTY: size_ub/2:

size_ub(X, Y)

The maximum size of the terms to which the argument Y is bound to is given by the expression Y. Various measures can be used to determine the size of an argument, e.g., list-length, term-size, term-depth, integer-value, etc. [DL93].

Usage: size_ub(X, Y)

• Description: Y is a upper bound on the size of argument X.

PROPERTY: steps_lb/2:

steps_lb(X, Y)

The minimum computation time (in resolution steps) spent by any call of the form X is given by the expression Y [DLGHL97,LGHD96]

Usage: steps_lb(X, Y)

• Description: Y is a lower bound on the cost of any call of the form X.

PROPERTY: steps_ub/2:

steps_ub(X, Y)

The maximum computation time (in resolution steps) spent by any call of the form X is given by the expression Y [DL93,LGHD96]

Usage: steps_ub(X, Y)

• Description: Y is a upper bound on the cost of any call of the form X.

PROPERTY: steps/2:

steps(X, Y)

The time (in resolution steps) spent by any call of the form X is given by the expression Y

Usage: steps(X, Y)

• Description: Y is the cost (number of resolution steps) of any call of the form X.

PROPERTY: finite_solutions/1:

finite_solutions(X)

Calls of the form X produce a finite number of solutions [DLGH97].

Usage: finite_solutions(X)

• Description: All the calls of the form X have a finite number of solutions.

PROPERTY: terminates/1:

terminates(X)

Calls of the form X always terminate [DLGH97].

Usage: terminates(X)

• Description: All the calls of the form X terminate.

PROPERTY: indep/1:

Usage: indep(X)

• Description: The variables in pairs in X are pairwise independent.
• The following properties hold globally: This predicate is understood natively by CiaoPP as indep(X). (basic_props:native/2)

PROPERTY: indep/2:

Usage: indep(X, Y)

• Description: X and Y do not have variables in common.
• The following properties hold globally: This predicate is understood natively by CiaoPP as indep([[X,Y]]). (basic_props:native/2)

PROPERTY: ground/1:

Usage: ground(X)

• Description: X is currently ground (it contains no variables).
• The following properties hold upon exit: X is ground. (basic_props:gnd/1)
• The following properties hold globally: X is not further instantiated. (basic_props:not_further_inst/2) This predicate is understood natively by CiaoPP. (basic_props:native/1)

PROPERTY: nonvar/1:

General properties: nonvar(X)

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

Usage: nonvar(X)

• Description: X is currently a term which is not a free variable.
• The following properties hold globally: X is not further instantiated. (basic_props:not_further_inst/2)

PROPERTY: var/1:

General properties: var(X)

• The following properties hold globally: This predicate is understood natively by CiaoPP. (basic_props:native/1) This predicate is understood natively by CiaoPP as free(X). (basic_props:native/2) var(X) is side-effect hard. (basic_props:sideff/2)

Usage: var(X)

• Description: X is a free variable.
• The following properties hold globally: X is not further instantiated. (basic_props:not_further_inst/2)

(UNDOC_REEXPORT): regtype/1:

Imported from basic_props (see the corresponding documentation for details).

(UNDOC_REEXPORT): native/2:

Imported from basic_props (see the corresponding documentation for details).

(UNDOC_REEXPORT): native/1:

Imported from basic_props (see the corresponding documentation for details).

(UNDOC_REEXPORT): sideff/2:

Imported from basic_props (see the corresponding documentation for details).

(UNDOC_REEXPORT): term/1:

Imported from basic_props (see the corresponding documentation for details).

(UNDOC_REEXPORT): int/1:

Imported from basic_props (see the corresponding documentation for details).

(UNDOC_REEXPORT): nnegint/1:

Imported from basic_props (see the corresponding documentation for details).

(UNDOC_REEXPORT): flt/1:

Imported from basic_props (see the corresponding documentation for details).

(UNDOC_REEXPORT): num/1:

Imported from basic_props (see the corresponding documentation for details).

(UNDOC_REEXPORT): atm/1:

Imported from basic_props (see the corresponding documentation for details).

(UNDOC_REEXPORT): struct/1:

Imported from basic_props (see the corresponding documentation for details).

(UNDOC_REEXPORT): gnd/1:

Imported from basic_props (see the corresponding documentation for details).

(UNDOC_REEXPORT): instance/2:

Imported from terms_check (see the corresponding documentation for details).

Go to the first, previous, next, last section, table of contents.