Properties which are native to analyzers

Author(s): Francisco Bueno, Manuel Hermenegildo, Pedro López, Edison Mera, Amadeo Casas.

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.

Documentation on exports

PROPERTYcompat/1

Usage:compat(Prop)

Use Prop as a compatibility property. Normally used with types. See the discussion in Declaring regular types.

  • The following properties should hold globally:
    (no_rtcheck/1)compat(Prop) is not checked during run-time checking.
Meta-predicate with arguments: compat(goal).

PROPERTYinstance/1

Usage:instance(Prop)

Use Prop as an instantiation property. Normally used with types. See the discussion in Declaring regular types.

  • The following properties should hold globally:
    (no_rtcheck/1)instance(Prop) is not checked during run-time checking.
Meta-predicate with arguments: instance(goal).

PROPERTYsucceeds/1

Usage:succeeds(Goal)

A call to Goal succeeds.

  • The following properties should hold globally:
    (no_rtcheck/1)succeeds(Goal) is not checked during run-time checking.
Meta-predicate with arguments: succeeds(goal).

PROPERTYmshare/1
mshare(X)

X contains all sharing sets [JL88,MH89b] 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)

The sharing pattern for the variables in the clause is X.

  • The following properties should hold globally:
    (native/2)This predicate is understood natively by CiaoPP as sharing(X).
    (no_rtcheck/1)mshare(X) is not checked during run-time checking.

PROPERTYindep/2

Usage:indep(X,Y)

X and Y do not have variables in common.

  • The following properties hold globally:
    (native/2)This predicate is understood natively by CiaoPP as indep([[X,Y]]).

PROPERTYindep/1

Usage:indep(X)

The variables in the the pairs in X are pairwise independent.

  • The following properties hold globally:
    (native/2)This predicate is understood natively by CiaoPP as indep(X).

PROPERTYcovered/2
covered(X,Y)

All variables occuring in X occur also in Y. Used by the non-strict independence-based annotators.

Usage:covered(X,Y)

X is covered by Y.

  • The following properties hold globally:
    (native/1)This predicate is understood natively by CiaoPP.

PROPERTYlinear/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)

X is instantiated to a linear term.

  • The following properties hold globally:
    (native/1)This predicate is understood natively by CiaoPP.

PROPERTYnonground/1

Usage:nonground(X)

X is not ground.

  • The following properties should hold globally:
    (native/2)This predicate is understood natively by CiaoPP as not_ground(X).

PROPERTYclique/1
clique(X)

X is a set of variables of interest, much the same as a sharing group but X represents all the sharing groups in the powerset of those variables. Similar to a sharing group, a clique is often translated to ground/1, indep/1, and indep/2 properties.

Usage:clique(X)

The clique sharing pattern is X.

  • The following properties should hold globally:
    (native/2)This predicate is understood natively by CiaoPP as clique(X).
    (no_rtcheck/1)clique(X) is not checked during run-time checking.

PROPERTYclique_1/1
clique_1(X)

X is a set of variables of interest, much the same as a sharing group but X represents all the sharing groups in the powerset of those variables but disregarding the singletons. Similar to a sharing group, a clique_1 is often translated to ground/1, indep/1, and indep/2 properties.

Usage:clique_1(X)

The 1-clique sharing pattern is X.

  • The following properties should hold globally:
    (native/2)This predicate is understood natively by CiaoPP as clique_1(X).
    (no_rtcheck/1)clique_1(X) is not checked during run-time checking.

PROPERTYis_det/1
is_det(X)

All calls of the form X are deterministic, i.e., produce at most one solution (or do not terminate). In other words, if X succeeds, it can only succeed once. It can still leave choice points after its execution, but when backtracking into these, it can only fail or go into an infinite loop. This property is inferred and checked natively by CiaoPP using the domains and techniques of [LGBH05,LGBH10].

Usage:is_det(X)

All calls of the form X are deterministic.

    Meta-predicate with arguments: is_det(goal).

    PROPERTYnon_det/1
    non_det(X)

    All calls of the form X are non-deterministic, i.e., they always produce more than one solution.

    Usage:non_det(X)

    All calls of the form X are non-deterministic.

      Meta-predicate with arguments: non_det(goal).

      possibly_nondet(X)

      Non-determinism is not ensured for calls of the form X. In other words, nothing can be ensured about determinacy of such calls. This is the default when no information is given for a predicate, so this property does not need to be stated explicitly.

      Usage:possibly_nondet(X)

      Non-determinism is not ensured for calls of the form X.

      • The following properties should hold globally:
        (no_rtcheck/1)possibly_nondet(X) is not checked during run-time checking.

      mut_exclusive(X)

      For any call of the form X at most one clause succeeds, i.e., clauses are pairwise exclusive. Note that determinacy is the transitive closure (to all called predicates) of this property. This property is inferred and checked natively by CiaoPP using the domains and techniques of [LGBH05,LGBH10].

      Usage:mut_exclusive(X)

      For any call of the form X at most one clause succeeds.

      • The following properties should hold globally:
        (rtcheck/2)The runtime check of this property is unimplemented.
      Meta-predicate with arguments: mut_exclusive(goal).

      not_mut_exclusive(X)

      For calls of the form X more than one clause may succeed. I.e., clauses are not disjoint for some call.

      Usage:not_mut_exclusive(X)

      For some calls of the form X more than one clause may succeed.

      • The following properties should hold globally:
        (rtcheck/2)The runtime check of this property is unimplemented.
      Meta-predicate with arguments: not_mut_exclusive(goal).

      possibly_not_mut_exclusive(X)

      Mutual exclusion of the clauses for calls of the form X cannot be ensured. This is the default when no information is given for a predicate, so this property does not need to be stated explicitly.

      Usage:possibly_not_mut_exclusive(X)

      Mutual exclusion is not ensured for calls of the form X.

      • The following properties should hold globally:
        (no_rtcheck/1)possibly_not_mut_exclusive(X) is not checked during run-time checking.
      Meta-predicate with arguments: possibly_not_mut_exclusive(goal).

      PROPERTYnot_fails/1
      not_fails(X)

      Calls of the form X produce at least one solution (succeed), or do not terminate. This property is inferred and checked natively by CiaoPP using the domains and techniques of [DLGH97,BLGH04].

      Usage:not_fails(X)

      All the calls of the form X do not fail.

      • The following properties hold globally:
        (native/1)This predicate is understood natively by CiaoPP.
      Meta-predicate with arguments: not_fails(goal).

      PROPERTYfails/1
      fails(X)

      Calls of the form X fail.

      Usage:fails(X)

      Calls of the form X fail.

      • The following properties hold globally:
        (native/1)This predicate is understood natively by CiaoPP.
      Meta-predicate with arguments: fails(goal).

      possibly_fails(X)

      Non-failure is not ensured for any call of the form X. In other words, nothing can be ensured about non-failure nor termination of such calls.

      Usage:possibly_fails(X)

      Non-failure is not ensured for calls of the form X.

      • The following properties should hold globally:
        (no_rtcheck/1)possibly_fails(X) is not checked during run-time checking.
      Meta-predicate with arguments: possibly_fails(goal).

      PROPERTYcovered/1
      covered(X)

      For any call of the form X there is at least one clause whose test (guard) succeeds (i.e., all the calls of the form X are covered). Note that nonfailure is the transitive closure (to all called predicates) of this property. [DLGH97,BLGH04].

      Usage:covered(X)

      All the calls of the form X are covered.

      • The following properties should hold globally:
        (rtcheck/2)The runtime check of this property is unimplemented.

      not_covered(X)

      There is some call of the form X for which there is no clause whose test succeeds [DLGH97].

      Usage:not_covered(X)

      Not all of the calls of the form X are covered.

      • The following properties should hold globally:
        (rtcheck/2)The runtime check of this property is unimplemented.

      possibly_not_covered(X)

      Covering is not ensured for any call of the form X. In other words, nothing can be ensured about covering of such calls.

      Usage:possibly_not_covered(X)

      Covering is not ensured for calls of the form X.

      • The following properties should hold globally:
        (no_rtcheck/1)possibly_not_covered(X) is not checked during run-time checking.
      Meta-predicate with arguments: possibly_not_covered(goal).

      PROPERTYtest_type/2

      Usage:test_type(X,T)

      Indicates the type of test that a predicate performs. Required by the nonfailure analyisis.

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

        Usage 1:num_solutions(X,N)

        Calls of the form X have N solutions, i.e., N is the cardinality of the solution set of X.

        • If the following properties should hold at call time:
          (callable/1)X is a term which represents a goal, i.e., an atom or a structure.
          (int/1)N is an integer.

        Usage 2:num_solutions(Goal,Check)

        For a call to Goal, Check(X) succeeds, where X is the number of solutions.

        • If the following properties should hold at call time:
          (callable/1)Goal is a term which represents a goal, i.e., an atom or a structure.
          (callable/1)Check is a term which represents a goal, i.e., an atom or a structure.

        PROPERTYrelations/2
        relations(X,N)

        Calls of the form X produce N solutions, i.e., N is the cardinality of the solution set of X.

        Usage:relations(X,N)

        Goal X produces N solutions.

        • If the following properties should hold at call time:
          (callable/1)X is a term which represents a goal, i.e., an atom or a structure.
          (int/1)N is an integer.
          then the following properties should hold globally:
          (rtcheck/2)The runtime check of this property is unimplemented.
        Meta-predicate with arguments: relations(goal,?).

        finite_solutions(X)

        Calls of the form X produce a finite number of solutions [DLGH97].

        Usage:finite_solutions(X)

        All the calls of the form X have a finite number of solutions.

        • The following properties should hold globally:
          (no_rtcheck/1)finite_solutions(X) is not checked during run-time checking.
        Meta-predicate with arguments: finite_solutions(goal).

        PROPERTYsolutions/2

        Usage:solutions(Goal,Sols)

        Goal Goal produces the solutions listed in Sols.

        • If the following properties should hold at call time:
          (callable/1)Goal is a term which represents a goal, i.e., an atom or a structure.
          (list/1)Sols is a list.

        Usage:cardinality(Prop,Lower,Upper)

        Prop has a number of solutions between Lower and Upper.

        • The following properties should hold globally:
          (no_rtcheck/1)cardinality(Prop,Lower,Upper) is not checked during run-time checking.

        Usage:no_choicepoints(X)

        A call to X does not leave new choicepoints.

          Meta-predicate with arguments: no_choicepoints(goal).

          Usage:leaves_choicepoints(X)

          A call to X leaves new choicepoints.

            Meta-predicate with arguments: leaves_choicepoints(goal).

            PROPERTYsize/2

            Usage:size(X,Y)

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

            • The following properties should hold globally:
              (no_rtcheck/1)size(X,Y) is not checked during run-time checking.

            PROPERTYsize/3

            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:
              (bound/1)A is a direction of approximation (upper or lower bound).
              then the following properties should hold globally:
              (no_rtcheck/1)size(A,X,Y) is not checked during run-time checking.

            PROPERTYsize_lb/2
            size_lb(X,Y)

            The minimum size of the terms to which the argument Y 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.

            • The following properties should hold globally:
              (no_rtcheck/1)size_lb(X,Y) is not checked during run-time checking.

            PROPERTYsize_ub/2
            size_ub(X,Y)

            The maximum size of the terms to which the argument Y 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.

            • The following properties should hold globally:
              (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 the expression Y.

            • The following properties should hold globally:
              (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.

            • Call and exit should be compatible with:
              (measure_t/1)Metric is a term size metric.
            • The following properties should hold globally:
              (no_rtcheck/1)size_metric(Head,Var,Metric) is not checked during run-time checking.
            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.

            • Call and exit should be compatible with:
              (bound/1)Approx is a direction of approximation (upper or lower bound).
              (measure_t/1)Metric is a term size metric.
            • The following properties should hold globally:
              (no_rtcheck/1)size_metric(Head,Approx,Var,Metric) is not checked during run-time checking.
            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.

              %% The size of the term is the number of rule %% applications of its type definition.

            • void: Used to indicate that the size of this argument should be ignored.

            Usage:measure_t(X)

            X is a term size metric.

              REGTYPEbound/1
              The types approximation (bounding) supported in size and cost analysis (see also resources_basic.pl).

              • upper: an upper bound.

              • lower: a lower bound.

              Usage:bound(X)

              X is a direction of approximation (upper or lower bound).

                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.

                • The following properties should hold globally:
                  (no_rtcheck/1)steps(X,Y) is not checked during run-time checking.
                Meta-predicate with arguments: steps(goal,?).

                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.

                • The following properties should hold globally:
                  (no_rtcheck/1)steps_lb(X,Y) is not checked during run-time checking.
                Meta-predicate with arguments: steps_lb(goal,?).

                PROPERTYsteps_o/2

                Usage:steps_o(X,Y)

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

                • The following properties should hold globally:
                  (no_rtcheck/1)steps_o(X,Y) is not checked during run-time checking.
                Meta-predicate with arguments: steps_o(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.

                • The following properties should hold globally:
                  (no_rtcheck/1)steps_ub(X,Y) is not checked during run-time checking.
                Meta-predicate with arguments: steps_ub(goal,?).

                PROPERTYrsize/2

                Usage:rsize(Var,SizeDescr)

                Var has its size defined by SizeDescr.

                • The following properties should hold globally:
                  (no_rtcheck/1)rsize(Var,SizeDescr) is not checked during run-time checking.

                PROPERTYcostb/4

                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.

                • The following properties should hold globally:
                  (no_rtcheck/1)costb(Goal,Resource,Lower,Upper) is not checked during run-time checking.

                PROPERTYterminates/1
                terminates(X)

                Calls of the form X always terminate.

                Usage:terminates(X)

                All calls of the form X terminate.

                • The following properties should hold globally:
                  (no_rtcheck/1)terminates(X) is not checked during run-time checking.
                Meta-predicate with arguments: terminates(goal).

                PROPERTYexception/1

                Usage:exception(Goal)

                Calls of the form Goal will throw an (unspecified) exception.

                  Meta-predicate with arguments: exception(goal).

                  PROPERTYexception/2

                  Usage:exception(Goal,E)

                  Calls to Goal will throw an exception that unifies with E.

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

                    Usage:possible_exceptions(Goal,Es)

                    Calls of the form Goal may throw exceptions, but only the ones that unify with the terms listed in Es.

                    • If the following properties should hold at call time:
                      (list/1)Es is a list.
                      then the following properties should hold globally:
                      (rtcheck/2)The runtime check of this property is unimplemented.
                    Meta-predicate with arguments: possible_exceptions(goal,?).

                    Usage:no_exception(Goal)

                    Calls of the form Goal do not throw any exception.

                      Meta-predicate with arguments: no_exception(goal).

                      Usage:no_exception(Goal,E)

                      Calls of the form Goal do not throw any exception that unifies with E.

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

                        PROPERTYsignal/1

                        Usage:signal(Goal)

                        Calls to Goal will send an (unspecified) signal.

                          Meta-predicate with arguments: signal(goal).

                          PROPERTYsignal/2

                          Usage:signal(Goal,E)

                          Calls to Goal will send a signal that unifies with E.

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

                            Usage:possible_signals(Goal,Es)

                            Calls of the form Goal may generate signals, but only the ones that unify with the terms listed in Es.

                            • The following properties should hold globally:
                              (rtcheck/2)The runtime check of this property is unimplemented.
                            Meta-predicate with arguments: possible_signals(goal,?).

                            PROPERTYno_signal/1

                            Usage:no_signal(Goal)

                            Calls of the form Goal do not send any signal.

                              Meta-predicate with arguments: no_signal(goal).

                              PROPERTYno_signal/2

                              Usage:no_signal(Goal,E)

                              Calls of the form Goal do not send any signals that unify with E.

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

                                Usage:sideff_hard(X)

                                X has hard side-effects, i.e., those that might affect program execution (e.g., assert/retract).

                                • The following properties should hold globally:
                                  (no_rtcheck/1)sideff_hard(X) is not checked during run-time checking.
                                Meta-predicate with arguments: sideff_hard(goal).

                                Usage:sideff_pure(X)

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

                                • The following properties should hold globally:
                                  (no_rtcheck/1)sideff_pure(X) is not checked during run-time checking.
                                Meta-predicate with arguments: sideff_pure(goal).

                                Usage:sideff_soft(X)

                                X has soft side-effects, i.e., those not affecting program execution (e.g., input/output).

                                • The following properties should hold globally:
                                  (no_rtcheck/1)sideff_soft(X) is not checked during run-time checking.
                                Meta-predicate with arguments: sideff_soft(goal).

                                PROPERTYconstraint/1
                                constraint(C)

                                C contains a list of linear (in)equalities that relate variables and int values. For example, [A < B + 4] is a constraint while [A < BC + 4] or [A = 3.4, B >= C] are not. Used by polyhedra-based analyses.

                                Usage:constraint(C)

                                C is a list of linear equations.

                                • The following properties hold globally:
                                  (native/1)This predicate is understood natively by CiaoPP.

                                PROPERTYtau/1
                                tau(Types)

                                Types contains a list with the type associations for each variable, in the form V/[T1,..,TN]. Note that tau is used in object-oriented programs only

                                Usage:tau(TypeInfo)

                                Types is a list of associations between variables and list of types

                                • The following properties hold globally:
                                  (native/1)This predicate is understood natively by CiaoPP.

                                Usage:user_output(Goal,S)

                                Calls of the form Goal write S to standard output.

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

                                  Documentation on imports

                                  This module has the following direct dependencies: