☰

*ON THIS PAGE*# Properties related to data sizes, cost, termination

These properties are part of the `native_props` library.

## Usage and interface

## Documentation on exports

`size(X,Y)`
`size(A,X,Y)`
`size(A,M,X,Y)`
`size_lb(X,Y)`
`size_ub(X,Y)`
*Meta-predicate* with arguments: `size_metric(goal,?,?)`.

*Meta-predicate* with arguments: `size_metric(goal,?,?,?)`.

`steps_lb(X,Y)`
*Meta-predicate* with arguments: `steps_lb(goal,?)`.

`steps_ub(X,Y)`
*Meta-predicate* with arguments: `steps_ub(goal,?)`.

`steps(X,Y)`
*Meta-predicate* with arguments: `steps(goal,?)`.

`steps_o(X,Y)`
*Meta-predicate* with arguments: `steps_o(goal,?)`.

`costb(Goal,Resource,Lower,Upper)`
*Meta-predicate* with arguments: `costb(goal,?,?,?)`.

`cost(Goal,Approx,Resource,Expr)`
*Meta-predicate* with arguments: `cost(goal,?,?,?)`.

`terminates(X)`
*Meta-predicate* with arguments: `terminates(goal)`.

## Documentation on imports

This module has the following direct dependencies:

- The Ciao System »

- PART III - Assertions and auto-documentation »

- Properties which are native to analyzers »

**Properties related to data sizes, cost, termination**

**Library usage:**`:- use_module(library(assertions/native_props))`or also as a package

`:- use_package(nativeprops)`.Note the slightly different names of the library and the package.

**Exports:***Properties:*`resource_id/1`,`size/2`,`size/3`,`size/4`,`size_lb/2`,`size_ub/2`,`size_o/2`,`size_metric/3`,`size_metric/4`,`steps_lb/2`,`steps_ub/2`,`steps/2`,`steps_o/2`,`rsize/2`,`costb/4`,`cost/4`,`terminates/1`.*Regular Types:*`approx/1`,`cost_expression/1`,`agg_expression/1`,`numeric_constant/1`,`size_term/1`,`indexvar/1`,`number_lattice/1`,`measure_t/1`.

REGTYPEapprox/1

The types of approximations (bounding) supported by the size and cost analyses (see also `resources_basic.pl`).

`ub`: for upper bounds.`lb`: for lower bounds.`exact`: for an exact expression.`o`: for the big-O.

Usage:`approx(X)`

X represents an approximation.

PROPERTYresource_id/1

A resource is a numerical property that varies (is used) throughout the execution of a piece of code. Resources can be predefined (i.e., in a library) or user-defined. Examples are computational (resolution) steps, time spent, energy consumed, memory usage, bytes sent over a wire, procedure calls, database operations, files left open, monetary units spent, disk space used, etc. See also `resources_decl`.

Usage:`resource_id(X)`

X is the name/identifier of a resource, either an atom or a compound term.

REGTYPEcost_expression/1

A cost expression is a symbolic function representing the cost of executing a piece of code in terms of the sizes of its input arguments and possibly other parameters. It is a term built from elements of the lattice of real numbers (see `number_lattice`), numerical constants (see `numeric_constant/1`), size metrics (see `size_metric`) and the following functors:

`- /1`: sign reversal.`+ /1`: identity.`-- /1`: decrement by one.`++ /1`: increment by one.`+ /2`: addition.`- /2`: subtraction.`* /2`: multiplication.`/ /2`: division.`** /2`: exponentiation.`exp/2`: exponentiation (DEPRECATED use`** /2`).`log/2`: logarithm given the base.`log10/1`: 10-base logarithm.`log2/1`: 2-base logarithm.`exp/1`: exponential (*e*to the power of).`log/1`: natural logarithm (base*e*).`sqrt/1`: square root.`fact/1`: factorial.`max/2`: maximum.`min/2`: minimum.`sum(Index,LowerBound,UpperBound,Exp)`: summation of all Exps obtained by instantiating index variable Index from LowerBound to UpperBound.`prod(Index,LowerBound,UpperBound,Exp)`: product of all Exps obtained by instantiating index variable Index from LowerBound to UpperBound.

Usage:`cost_expression(X)`

X is a cost expression.

REGTYPEagg_expression/1

An aggregation expression is an expression appearing in an aggregation function (`sum/4`, `prod/4`). An aggregation expression can be a regular cost expression (see `cost_expression/1`) or it may include index variables as well (see `indexvar/1`).

Usage:`agg_expression(X)`

X is an aggregation expression.

REGTYPEnumeric_constant/1

A numeric constant is a fixed, well-defined real number.

Currently supported constants:

`e`: Euler's number.

Usage:`numeric_constant(X)`

X represents a numeric constant.

REGTYPEsize_term/1

A size term is a term in a cost expression (see `cost_expression/1`) representing the size of a term in a given metric (see `measure_t/1`).

Usage:`size_term(X)`

X represents the size of a term.

REGTYPEindexvar/1

A variable used as an index in an aggregation expression.

Usage:`indexvar(X)`

X is an index variable.

REGTYPEnumber_lattice/1

A lattice containing real numbers, `inf` and `bot`.

Usage:`number_lattice(X)`

X is a number, `inf` or `bot`.

PROPERTYsize/2

The exact size (for any approximation) of term X is given by expression Y, which may depend on the size of other terms. `size(X,Y)` is equivalent to `size(exact,X,Y)`.

Usage:`size(X,Y)`

Y is the size of argument X, for any approximation.

*If the following properties should hold at call time:*

(`basic_props:term/1`)X is any term.

(`user(... /native_props_cost_doc):cost_expression/1`)Y is a cost expression.*then the following properties should hold globally:*

(`basic_props:no_rtcheck/1`)size(X,Y) is not checked during run-time checking.

PROPERTYsize/3

The size of term X for the approximation A is given by expression Y, which may depend on the size of other terms.

Usage:`size(A,X,Y)`

Y is the size of argument X, for the approximation A.

*If the following properties should hold at call time:*

(`user(... /native_props_cost_doc):approx/1`)A represents an approximation.

(`basic_props:term/1`)X is any term.

(`user(... /native_props_cost_doc):cost_expression/1`)Y is a cost expression.*then the following properties should hold globally:*

(`basic_props:no_rtcheck/1`)size(A,X,Y) is not checked during run-time checking.

PROPERTYsize/4

The size of term X, measured in metric M, for the approximation A is given by expression Y, which may depend on the size of other terms.

Usage:`size(A,M,X,Y)`

Y is the size of argument X measured in M, for the approximation A.

*If the following properties should hold at call time:*

(`user(... /native_props_cost_doc):approx/1`)A represents an approximation.

(`user(... /native_props_cost_doc):measure_t/1`)M is a term size metric.

(`basic_props:term/1`)X is any term.

(`user(... /native_props_cost_doc):cost_expression/1`)Y is a cost expression.*then the following properties should hold globally:*

(`basic_props:no_rtcheck/1`)size(A,M,X,Y) is not checked during run-time checking.

PROPERTYsize_lb/2

The minimum size of the terms to which the argument X is bound 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,LGHD96]. See `measure_t/1`.

Usage:`size_lb(X,Y)`

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

*If the following properties should hold at call time:*

(`basic_props:term/1`)X is any term.

(`user(... /native_props_cost_doc):cost_expression/1`)Y is a cost expression.*then the following properties should hold globally:*

(`basic_props:no_rtcheck/1`)size_lb(X,Y) is not checked during run-time checking.

PROPERTYsize_ub/2

The maximum size of the terms to which the argument X is bound 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,LGHD96]. See `measure_t/1`.

Usage:`size_ub(X,Y)`

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

*If the following properties should hold at call time:*

(`basic_props:term/1`)X is any term.

(`user(... /native_props_cost_doc):cost_expression/1`)Y is a cost expression.*then the following properties should hold globally:*

(`basic_props:no_rtcheck/1`)size_ub(X,Y) is not checked during run-time checking.

PROPERTYsize_o/2

Usage:`size_o(X,Y)`

The size of argument X is in the order of expression Y.

*If the following properties should hold at call time:*

(`basic_props:term/1`)X is any term.

(`user(... /native_props_cost_doc):cost_expression/1`)Y is a cost expression.*then the following properties should hold globally:*

(`basic_props:no_rtcheck/1`)size_o(X,Y) is not checked during run-time checking.

PROPERTYsize_metric/3

Usage:`size_metric(Head,Var,Metric)`

Metric is the measure used to determine the size of the terms that Var is bound to, for any type of approximation.

*If the following properties should hold at call time:*

(`basic_props:cgoal/1`)Head is a term which represents a goal, i.e., an atom or a structure.

(`basic_props:term/1`)Var is any term.

(`user(... /native_props_cost_doc):measure_t/1`)Metric is a term size metric.*then the following properties should hold globally:*

(`basic_props:no_rtcheck/1`)size_metric(Head,Var,Metric) is not checked during run-time checking.

PROPERTYsize_metric/4

Usage:`size_metric(Head,Approx,Var,Metric)`

Metric is the measure used to determine the size of the terms that variable Var bound to, for the approximation Approx.

*If the following properties should hold at call time:*

(`basic_props:cgoal/1`)Head is a term which represents a goal, i.e., an atom or a structure.

(`user(... /native_props_cost_doc):approx/1`)Approx represents an approximation.

(`basic_props:term/1`)Var is any term.

(`user(... /native_props_cost_doc):measure_t/1`)Metric is a term size metric.*then the following properties should hold globally:*

(`basic_props:no_rtcheck/1`)size_metric(Head,Approx,Var,Metric) is not checked during run-time checking.

REGTYPEmeasure_t/1

The types of term size measures currently supported in size and cost analysis (see also in `resources_basic.pl`).

`int`: The size of the term (which is an integer) is the integer value itself.`length`: The size of the term (which is a list) is its length.`size`: The size is the overall of the term (number of subterms).`depth([_|_])`: The size of the term is its depth.`void`: Used to indicate that the size of this argument should be ignored.

Usage:`measure_t(X)`

X is a term size metric.

PROPERTYsteps_lb/2

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

Usage:`steps_lb(X,Y)`

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

*If the following properties should hold at call time:*

(`basic_props:cgoal/1`)X is a term which represents a goal, i.e., an atom or a structure.

(`user(... /native_props_cost_doc):cost_expression/1`)Y is a cost expression.*then the following properties should hold globally:*

(`basic_props:no_rtcheck/1`)steps_lb(X,Y) is not checked during run-time checking.

PROPERTYsteps_ub/2

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

Usage:`steps_ub(X,Y)`

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

*If the following properties should hold at call time:*

(`basic_props:cgoal/1`)X is a term which represents a goal, i.e., an atom or a structure.

(`user(... /native_props_cost_doc):cost_expression/1`)Y is a cost expression.*then the following properties should hold globally:*

(`basic_props:no_rtcheck/1`)steps_ub(X,Y) is not checked during run-time checking.

PROPERTYsteps/2

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

Usage:`steps(X,Y)`

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

*If the following properties should hold at call time:*

(`basic_props:cgoal/1`)X is a term which represents a goal, i.e., an atom or a structure.

(`user(... /native_props_cost_doc):cost_expression/1`)Y is a cost expression.*then the following properties should hold globally:*

(`basic_props:no_rtcheck/1`)steps(X,Y) is not checked during run-time checking.

PROPERTYsteps_o/2

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

Usage:`steps_o(X,Y)`

Y is the complexity order of the cost of any call of the form X.

*If the following properties should hold at call time:*

(`basic_props:cgoal/1`)X is a term which represents a goal, i.e., an atom or a structure.

(`user(... /native_props_cost_doc):cost_expression/1`)Y is a cost expression.*then the following properties should hold globally:*

(`basic_props:no_rtcheck/1`)steps_o(X,Y) is not checked during run-time checking.

PROPERTYrsize/2

Usage:`rsize(Var,SizeDescr)`

Var has its size defined by SizeDescr.

*The following properties should hold globally:*

(`basic_props:no_rtcheck/1`)rsize(Var,SizeDescr) is not checked during run-time checking.

PROPERTYcostb/4

Lower (res. Upper) is a (safe) lower (res. upper) bound on the cost of the computation of Goal in terms of Resource units.

Usage:`costb(Goal,Resource,Lower,Upper)`

Lower (resp. Upper) is a (safe) lower (resp. upper) bound on the cost of the computation of Goal expressed in terms of Resource units.

*If the following properties should hold at call time:*

(`basic_props:cgoal/1`)Goal is a term which represents a goal, i.e., an atom or a structure.

(`user(... /native_props_cost_doc):resource_id/1`)Resource is the name/identifier of a resource, either an atom or a compound term.

(`user(... /native_props_cost_doc):cost_expression/1`)Lower is a cost expression.

(`user(... /native_props_cost_doc):cost_expression/1`)Upper is a cost expression.*then the following properties should hold globally:*

(`basic_props:no_rtcheck/1`)costb(Goal,Resource,Lower,Upper) is not checked during run-time checking.

PROPERTYcost/4

Expr is a (safe) upper or lower bounds, depending on the value of Approx (see `approx/1`), of the cost of computation of the goal Goal in terms of Resource units.

Usage:`cost(Goal,Approx,Resource,Expr)`

Expr is a safe upper or lower bounds (depending on Approx) of the cost of computing Goal in terms of Resource units.

*If the following properties should hold at call time:*

(`basic_props:cgoal/1`)Goal is a term which represents a goal, i.e., an atom or a structure.

(`user(... /native_props_cost_doc):approx/1`)Approx represents an approximation.

(`user(... /native_props_cost_doc):resource_id/1`)Resource is the name/identifier of a resource, either an atom or a compound term.

(`user(... /native_props_cost_doc):cost_expression/1`)Expr is a cost expression.*then the following properties should hold globally:*

(`basic_props:no_rtcheck/1`)cost(Goal,Approx,Resource,Expr) is not checked during run-time checking.

PROPERTYterminates/1

Calls of the form X always terminate.

Usage:`terminates(X)`

All calls of the form X terminate.

*If the following properties should hold at call time:*

(`basic_props:cgoal/1`)X is a term which represents a goal, i.e., an atom or a structure.*then the following properties should hold globally:*

(`basic_props:no_rtcheck/1`)terminates(X) is not checked during run-time checking.

*Packages:*`prelude`,`initial`,`condcomp`,`assertions`,`assertions/assertions_basic`,`regtypes`.

Generated with LPdoc using Ciao