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

**Version:** 1.10#6 (2004/8/7, 21:46:39 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.

`native_props`

)**Library usage:**`:- use_module(library('assertions/native_props'))`

or also as a package`:- use_package(nativeprops)`

. Note the different names of the library and the package.**Exports:****Other modules used:**

`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:*

is not ground.`X`

*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

are pairwise independent.`X`

*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.