Properties which are native to analyzers

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

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

PROPERTY
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 pattern is X.

  • The following properties should hold globally:
    (basic_props:native/2)This predicate is understood natively by CiaoPP as clique(X).
    (basic_props:no_rtcheck/1)Declares that the assertion in which this comp property appears must not be checked at run-time. Equivalent to rtcheck(G, impossible).

PROPERTY
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 pattern is X.

  • The following properties should hold globally:
    (basic_props:native/2)This predicate is understood natively by CiaoPP as clique_1(X).
    (basic_props:no_rtcheck/1)Declares that the assertion in which this comp property appears must not be checked at run-time. Equivalent to rtcheck(G, impossible).

PROPERTY

Usage:compat(Prop)

Use Prop as a compatibility property.

  • The following properties should hold globally:
    (basic_props:no_rtcheck/1)Declares that the assertion in which this comp property appears must not be checked at run-time. Equivalent to rtcheck(G, impossible).
Meta-predicate with arguments: compat(goal).

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

(True) Usage:constraint(C)

C is a list of linear equations

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

PROPERTY
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)

All the calls of the form X are covered.

  • The following properties should hold globally:
    (basic_props:rtcheck/2)The runtime check of the property have the status unimplemented.

PROPERTY
covered(X,Y)

All variables occuring in X occur also in Y.

(True) Usage:covered(X,Y)

X is covered by Y.

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

PROPERTY

Usage:exception(Goal)

Calls of the form Goal throw an exception.

    Meta-predicate with arguments: exception(goal).

    PROPERTY

    Usage:exception(Goal,E)

    Calls of the form Goal throw an exception that unifies with E.

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

      PROPERTY
      fails(X)

      Calls of the form X fail.

      (True) Usage:fails(X)

      Calls of the form X fail.

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

      PROPERTY
      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:
        (basic_props:no_rtcheck/1)Declares that the assertion in which this comp property appears must not be checked at run-time. Equivalent to rtcheck(G, impossible).
      Meta-predicate with arguments: finite_solutions(goal).

      PROPERTY

      Usage:have_choicepoints(X)

      A call to X creates choicepoints.

        Meta-predicate with arguments: have_choicepoints(goal).

        PROPERTY

        (True) Usage:indep(X)

        The variables in pairs in X are pairwise independent.

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

        PROPERTY

        (True) Usage:indep(X,Y)

        X and Y do not have variables in common.

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

        PROPERTY

        Usage:instance(Prop)

        Use Prop as an instantiation property. Verify that execution of Prop does not produce bindings for the argument variables.

        • The following properties should hold globally:
          (basic_props:no_rtcheck/1)Declares that the assertion in which this comp property appears must not be checked at run-time. Equivalent to rtcheck(G, impossible).
        Meta-predicate with arguments: instance(goal).

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

        Usage:is_det(X)

        All calls of the form X are deterministic.

          Meta-predicate with arguments: is_det(goal).

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

          (True) Usage:linear(X)

          X is instantiated to a linear term.

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

          PROPERTY
          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)

          The sharing pattern is X.

          • The following properties should hold globally:
            (basic_props:native/2)This predicate is understood natively by CiaoPP as sharing(X).
            (basic_props:no_rtcheck/1)Declares that the assertion in which this comp property appears must not be checked at run-time. Equivalent to rtcheck(G, impossible).
          General properties:

          Test:mshare(L)

          • If the following properties should hold at call time:
            (term_basic:= /2)term_basic:L=[[A],[p(A)]]
            then the following properties should hold globally:
            (native_props:fails/1)Calls of the form mshare(L) fail.

          Test:mshare(L)

          • If the following properties should hold at call time:
            (term_basic:= /2)term_basic:L=[[A],[p(B)]]
            then the following properties should hold globally:
            (native_props:not_fails/1)All the calls of the form mshare(L) do not fail.

          PROPERTY
          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)

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

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

          PROPERTY

          Usage:no_choicepoints(X)

          A call to X does not create choicepoints.

            Meta-predicate with arguments: no_choicepoints(goal).

            PROPERTY

            Usage:no_exception(Goal)

            Calls of the form Goal do not throw any exception.

              Meta-predicate with arguments: no_exception(goal).

              PROPERTY

              Usage:no_exception(Goal,E)

              Calls of the form Goal do not throw exception E.

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

                PROPERTY

                Usage:no_signal(Goal)

                Calls of the form Goal do not send any signal.

                  Meta-predicate with arguments: no_signal(goal).

                  PROPERTY

                  Usage:no_signal(Goal,E)

                  Calls of the form Goal do not send the signal E.

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

                    PROPERTY
                    non_det(X)

                    All calls of the form X are non-deterministic, i.e., produce several solutions.

                    Usage:non_det(X)

                    All calls of the form X are non-deterministic.

                      Meta-predicate with arguments: non_det(goal).

                      PROPERTY

                      Usage:nonground(X)

                      X is not ground.

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

                      PROPERTY
                      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:
                        (basic_props:rtcheck/2)The runtime check of the property have the status unimplemented.

                      PROPERTY
                      not_fails(X)

                      Calls of the form X produce at least one solution, or do not terminate [DLGH97].

                      (True) Usage:not_fails(X)

                      All the calls of the form X do not fail.

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

                      PROPERTY
                      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:
                        (basic_props:rtcheck/2)The runtime check of the property have the status unimplemented.
                      Meta-predicate with arguments: not_mut_exclusive(goal).

                      PROPERTY

                      Usage 1:num_solutions(X,N)

                      All the calls of the form X have N solutions.

                      • If the following properties should hold at call time:
                        (basic_props:callable/1)X is a term which represents a goal, i.e., an atom or a structure.
                        (basic_props: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:
                        (basic_props:callable/1)Goal is a term which represents a goal, i.e., an atom or a structure.
                        (basic_props:callable/1)Check is a term which represents a goal, i.e., an atom or a structure.

                      PROPERTY

                      Usage:solutions(Goal,Sols)

                      Goal Goal produces the solutions listed in Sols.

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

                      PROPERTY
                      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)

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

                      • The following properties should hold globally:
                        (basic_props:no_rtcheck/1)Declares that the assertion in which this comp property appears must not be checked at run-time. Equivalent to rtcheck(G, impossible).
                      Meta-predicate with arguments: possibly_fails(goal).

                      PROPERTY
                      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)

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

                      • The following properties should hold globally:
                        (basic_props:no_rtcheck/1)Declares that the assertion in which this comp property appears must not be checked at run-time. Equivalent to rtcheck(G, impossible).

                      PROPERTY
                      relations(X,N)

                      The goal X produces N solutions. In other words, N is the cardinality of the solution set of X.

                      Usage:relations(X,N)

                      Goal X produces N solutions.

                      • The following properties should hold globally:
                        (basic_props:rtcheck/2)The runtime check of the property have the status unimplemented.
                      Meta-predicate with arguments: relations(goal,?).

                      PROPERTY

                      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:
                        (basic_props:no_rtcheck/1)Declares that the assertion in which this comp property appears must not be checked at run-time. Equivalent to rtcheck(G, impossible).
                      Meta-predicate with arguments: sideff_hard(goal).

                      PROPERTY

                      Usage:sideff_pure(X)

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

                      • The following properties should hold globally:
                        (basic_props:no_rtcheck/1)Declares that the assertion in which this comp property appears must not be checked at run-time. Equivalent to rtcheck(G, impossible).
                      Meta-predicate with arguments: sideff_pure(goal).

                      PROPERTY

                      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:
                        (basic_props:no_rtcheck/1)Declares that the assertion in which this comp property appears must not be checked at run-time. Equivalent to rtcheck(G, impossible).
                      Meta-predicate with arguments: sideff_soft(goal).

                      PROPERTY

                      Usage:signal(Goal)

                      Calls of the form Goal throw a signal.

                        Meta-predicate with arguments: signal(goal).

                        PROPERTY

                        Usage:signal(Goal,E)

                        A call to Goal sends a signal that unifies with E.

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

                          PROPERTY

                          Usage:signals(Goal,Es)

                          Calls of the form Goal can generate only the signals that unify with the terms listed in Es.

                          • The following properties should hold globally:
                            (basic_props:rtcheck/2)The runtime check of the property have the status unimplemented.
                          Meta-predicate with arguments: signals(goal,?).

                          PROPERTY

                          Usage:size(X,Y)

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

                          • The following properties should hold globally:
                            (basic_props:no_rtcheck/1)Declares that the assertion in which this comp property appears must not be checked at run-time. Equivalent to rtcheck(G, impossible).

                          PROPERTY

                          Usage:size(A,X,Y)

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

                          • The following properties should hold globally:
                            (basic_props:no_rtcheck/1)Declares that the assertion in which this comp property appears must not be checked at run-time. Equivalent to rtcheck(G, impossible).

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

                          Usage:size_lb(X,Y)

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

                          • The following properties should hold globally:
                            (basic_props:no_rtcheck/1)Declares that the assertion in which this comp property appears must not be checked at run-time. Equivalent to rtcheck(G, impossible).

                          PROPERTY

                          Usage:size_o(X,Y)

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

                          • The following properties should hold globally:
                            (basic_props:no_rtcheck/1)Declares that the assertion in which this comp property appears must not be checked at run-time. Equivalent to rtcheck(G, impossible).

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

                          Usage:size_ub(X,Y)

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

                          • The following properties should hold globally:
                            (basic_props:no_rtcheck/1)Declares that the assertion in which this comp property appears must not be checked at run-time. Equivalent to rtcheck(G, impossible).

                          PROPERTY

                          Usage:size_metric(Head,Var,Metric)

                          Metric is the metric of the variable Var, for any approximation.

                          • The following properties should hold globally:
                            (basic_props:no_rtcheck/1)Declares that the assertion in which this comp property appears must not be checked at run-time. Equivalent to rtcheck(G, impossible).
                          Meta-predicate with arguments: size_metric(goal,?,?).

                          PROPERTY

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

                          Metric is the metric of the variable Var, for the approximation Approx. Currently, Metric can be: int/1, size/1, length/1, depth/2, and void/1.

                          • The following properties should hold globally:
                            (basic_props:no_rtcheck/1)Declares that the assertion in which this comp property appears must not be checked at run-time. Equivalent to rtcheck(G, impossible).
                          Meta-predicate with arguments: size_metric(goal,?,?,?).

                          PROPERTY

                          Usage:succeeds(Prop)

                          A call to Prop succeeds.

                          • The following properties should hold globally:
                            (basic_props:no_rtcheck/1)Declares that the assertion in which this comp property appears must not be checked at run-time. Equivalent to rtcheck(G, impossible).
                          Meta-predicate with arguments: succeeds(goal).

                          PROPERTY
                          steps(X,Y)

                          The time (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:
                            (basic_props:no_rtcheck/1)Declares that the assertion in which this comp property appears must not be checked at run-time. Equivalent to rtcheck(G, impossible).
                          Meta-predicate with arguments: steps(goal,?).

                          PROPERTY
                          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)

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

                          • The following properties should hold globally:
                            (basic_props:no_rtcheck/1)Declares that the assertion in which this comp property appears must not be checked at run-time. Equivalent to rtcheck(G, impossible).
                          Meta-predicate with arguments: steps_lb(goal,?).

                          PROPERTY

                          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:
                            (basic_props:no_rtcheck/1)Declares that the assertion in which this comp property appears must not be checked at run-time. Equivalent to rtcheck(G, impossible).
                          Meta-predicate with arguments: steps_o(goal,?).

                          PROPERTY
                          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)

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

                          • The following properties should hold globally:
                            (basic_props:no_rtcheck/1)Declares that the assertion in which this comp property appears must not be checked at run-time. Equivalent to rtcheck(G, impossible).
                          Meta-predicate with arguments: steps_ub(goal,?).

                          PROPERTY
                          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

                          (True) Usage:tau(TypeInfo)

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

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

                          PROPERTY
                          terminates(X)

                          Calls of the form X always terminate [DLGH97].

                          Usage:terminates(X)

                          All calls of the form X terminate.

                          • The following properties should hold globally:
                            (basic_props:no_rtcheck/1)Declares that the assertion in which this comp property appears must not be checked at run-time. Equivalent to rtcheck(G, impossible).
                          Meta-predicate with arguments: terminates(goal).

                          PROPERTY

                          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,?).

                            PROPERTY

                            Usage:throws(Goal,Es)

                            Calls of the form Goal can throw only the exceptions that unify with the terms listed in Es.

                            • The following properties should hold globally:
                              (basic_props:rtcheck/2)The runtime check of the property have the status unimplemented.
                            Meta-predicate with arguments: throws(goal,?).

                            PROPERTY

                            Usage:user_output(Goal,S)

                            Calls of the form Goal write S to standard output.

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

                              PROPERTY

                              (True) Usage:instance(Term1,Term2)

                              Term1 is an instance of Term2.

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

                              Known bugs and planned improvements

                              • A missing property is succeeds (not_fails = succeeds or not_terminates. -- EMM