Properties related to data sizes, cost, termination

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

Usage:resource_id(X)

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

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

Usage:agg_expression(X)

X is an aggregation expression.

Currently supported constants:

• e: Euler's number.

Usage:numeric_constant(X)

X represents a numeric constant.

Usage:size_term(X)

X represents the size of a term.

Usage:indexvar(X)

X is an index variable.

Usage:number_lattice(X)

X is a number, inf or bot.

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.

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.

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.

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.

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.

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.

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.

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.

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

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.

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.

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.

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.

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.

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.

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.

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.