Properties related to data sizes, cost, termination

These properties are part of the native_props library.

Usage and interface

Documentation on exports

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.

    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.

      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:

      Usage:cost_expression(X)

      X is a cost expression.

        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.

          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.

            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.

                A lattice containing real numbers, inf and bot.

                Usage:number_lattice(X)

                X is a number, inf or bot.

                  PROPERTYsize/2
                  size(X,Y)

                  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.

                  PROPERTYsize/3
                  size(A,X,Y)

                  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.

                  PROPERTYsize/4
                  size(A,M,X,Y)

                  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.

                  PROPERTYsize_lb/2
                  size_lb(X,Y)

                  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.

                  PROPERTYsize_ub/2
                  size_ub(X,Y)

                  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.

                  PROPERTYsize_o/2

                  Usage:size_o(X,Y)

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

                  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.

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

                  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.

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

                  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
                    steps_lb(X,Y)

                    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.

                    Meta-predicate with arguments: steps_lb(goal,?).

                    PROPERTYsteps_ub/2
                    steps_ub(X,Y)

                    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.

                    Meta-predicate with arguments: steps_ub(goal,?).

                    PROPERTYsteps/2
                    steps(X,Y)

                    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.

                    Meta-predicate with arguments: steps(goal,?).

                    PROPERTYsteps_o/2
                    steps_o(X,Y)

                    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.

                    Meta-predicate with arguments: steps_o(goal,?).

                    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
                    costb(Goal,Resource,Lower,Upper)

                    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.

                    Meta-predicate with arguments: costb(goal,?,?,?).

                    PROPERTYcost/4
                    cost(Goal,Approx,Resource,Expr)

                    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.

                    Meta-predicate with arguments: cost(goal,?,?,?).

                    PROPERTYterminates/1
                    terminates(X)

                    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.
                    Meta-predicate with arguments: terminates(goal).

                    Documentation on imports

                    This module has the following direct dependencies: