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

**Version:** 1.7#208 (2002/4/23, 19:9:14 CEST)

**Version of last change:** 1.5#1 (1999/11/29, 17:12:34 MET)

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

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

- PROPERTY:
**fails/1:** -
`fails(X)`

Calls of the form

`X`

fail.**Usage:**`fails(X)`

*Description:*Calls of the form`X`

fail.

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

- 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:
**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:
**sideff_pure/1:** -
**Usage:**`sideff_pure(X)`

*Description:*`X`

is pure, i.e., has no side-effects.

- PROPERTY:
**sideff_soft/1:** -
**Usage:**`sideff_soft(X)`

- PROPERTY:
**sideff_hard/1:** -
**Usage:**`sideff_hard(X)`

- PREDICATE:
**indep/1:** -
**Usage:**`indep(X)`

*Description:*The variables in pairs in

are pairwise independent.`X`

- PROPERTY:
**indep/2:** -
**Usage:**`indep(X,Y)`

*Description:*`X`

and`Y`

do not have variables in common.

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