Types and properties related to assertions

Author(s): Manuel Hermenegildo.

Version: 1.10#7 (2006/4/26, 19:22:13 CEST)

Version of last change: 1.7#156 (2001/11/24, 13:23:30 CET)

This module is part of the assertions library. It provides the formal definition of the syntax of several forms of assertions and describes their meaning. It does so by defining types and properties related to the assertions themselves. The text describes, for example, the overall fields which are admissible in the bodies of assertions, where properties can be used inside these bodies, how to combine properties for a given predicate argument (e.g., conjunctions) , etc. and provides some examples.

• Usage and interface (assertions_props)
• Documentation on exports (assertions_props)

Usage and interface (assertions_props)

Documentation on exports (assertions_props)

REGTYPE: assrt_body/1:

This predicate defines the different types of syntax admissible in the bodies of pred/1, decl/1, etc. assertions. Such a body is of the form:

      Pr [:: DP] [: CP] [=> AP] [+ GP] [# CO]

where (fields between [...] are optional):

• Pr is a head pattern ( head_pattern/1) which describes the predicate or property and possibly gives some implicit call/answer information.
• DP is a (possibly empty) complex argument property ( complex_arg_property/1) which expresses properties which are compatible with the predicate, i.e., instantiations made by the predicate are compatible with the properties in the sense that applying the property at any point to would not make it fail.
• CP is a (possibly empty) complex argument property ( complex_arg_property/1) which applies to the calls to the predicate.
• AP is a (possibly empty) complex argument property ( complex_arg_property/1) which applies to the answers to the predicate (if the predicate succeeds). These only apply if the (possibly empty) properties given for calls in the assertion hold.
• GP is a (possibly empty) complex goal property ( complex_goal_property/1) which applies to the whole execution of a call to the predicate. These only apply if the (possibly empty) properties given for calls in the assertion hold.
• CO is a comment string ( docstring/1). This comment only applies if the (possibly empty) properties given for calls in the assertion hold. The usual formatting commands that are applicable in comment strings can be used (see stringcommand/1). See the lpdoc manual for documentation on assertion comments.

Usage: assrt_body(X)

• Description: X is an assertion body.

PROPERTY: head_pattern/1:

A head pattern can be a predicate name (functor/arity) ( predname/1) or a term. Thus, both p/3 and p(A,B,C) are valid head patterns. In the case in which the head pattern is a term, each argument of such a term can be:

• A variable. This is useful in order to be able to refer to the corresponding argument positions by name within properties and in comments. Thus, p(Input,Parameter,Output) is a valid head pattern.
• A ground term. In this case this term determines a property of the corresponding argument. The actual property referred to is that given by the term but with one more argument added at the beginning, which is a new variable which, in a rewriting of the head pattern, appears at the argument position occupied by the term. Unless otherwise stated (see below), the property built this way is understood to hold for both calls and answers. For example, the head pattern p(Input,list(integer),Output) is valid and equivalent for example to having the head pattern p(Input,A,Output) and stating that the property list(A,integer) holds for the calls and successes of the predicate.
• Finally, it can also be a variable or a ground term, as above, but preceded by a " mode." This mode determines in a compact way certain call or answer properties. For example, the head pattern p(Input,+list(integer),Output) is valid, as long as +/1 is declared as a mode. Acceptable modes are documented in library(modes). User defined modes are documented in modedef/1.

Usage: head_pattern(Pr)

• Description: Pr is a head pattern.

REGTYPE: complex_arg_property/1:

complex_arg_property(Props)

Props is a (possibly empty) complex argument property. Such properties can appear in two formats, which are defined by property_conjunction/1 and property_starterm/1 respectively. The two formats can be mixed provided they are not in the same field of an assertion. I.e., the following is a valid assertion:

:- pred foo(X,Y) : nonvar * var => (ground(X),ground(Y)).

Usage: complex_arg_property(Props)

• Description: Props is a (possibly empty) complex argument property

REGTYPE: property_conjunction/1:

This type defines the first, unabridged format in which properties can be expressed in the bodies of assertions. It is essentially a conjunction of properties which refer to variables. The following is an example of a complex property in this format:

• (integer(X),list(Y,integer)): X has the property integer/1 and Y has the property list/2, with second argument integer.

Usage: property_conjunction(Props)

• Description: Props is either a term or a conjunction of terms. The main functor and arity of each of those terms corresponds to the definition of a property. The first argument of each such term is a variable which appears as a head argument.

REGTYPE: property_starterm/1:

This type defines a second, compact format in which properties can be expressed in the bodies of assertions. A property_starterm/1 is a term whose main functor is */2 and, when it appears in an assertion, the number of terms joined by */2 is exactly the arity of the predicate it refers to. A similar series of properties as in property_conjunction/1 appears, but the arity of each property is one less: the argument position to which they refer (first argument) is left out and determined by the position of the property in the property_starterm/1. The idea is that each element of the */2 term corresponds to a head argument position. Several properties can be assigned to each argument position by grouping them in curly brackets. The following is an example of a complex property in this format:

• integer * list(integer): the first argument of the procedure (or function, or ...) has the property integer/1 and the second one has the property list/2, with second argument integer.
• {integer,var} * list(integer): the first argument of the procedure (or function, or ...) has the properties integer/1 and var/1 and the second one has the property list/2, with second argument integer.

Usage: property_starterm(Props)

• Description: Props is either a term or several terms separated by */2. The main functor of each of those terms corresponds to that of the definition of a property, and the arity should be one less than in the definition of such property. All arguments of each such term are ground.

REGTYPE: complex_goal_property/1:

complex_goal_property(Props)

Props is a (possibly empty) complex goal property. Such properties can be either a term or a conjunction of terms. The main functor and arity of each of those terms corresponds to the definition of a property. Such properties apply to all executions of all goals of the predicate which comply with the assertion in which the Props appear.

The arguments of the terms in Props are implicitely augmented with a first argument which corresponds to a goal of the predicate of the assertion in which the Props appear. For example, the assertion

     :- comp var(A) + not_further_inst(A).

has property not_further_inst/1 as goal property, and establishes that in all executions of var(A) it should hold that not_further_inst(var(A),A).

Usage: complex_goal_property(Props)

• Description: Props is either a term or a conjunction of terms. The main functor and arity of each of those terms corresponds to the definition of a property. A first implicit argument in such terms identifies goals to which the properties apply.

PROPERTY: nabody/1:

Usage: nabody(ABody)

• Description: ABody is a normalized assertion body.

REGTYPE: dictionary/1:

Usage: dictionary(D)

• Description: D is a dictionary of variable names.

REGTYPE: c_assrt_body/1:

This predicate defines the different types of syntax admissible in the bodies of call/1, entry/1, etc. assertions. The following are admissible:

      Pr : CP [# CO]

where (fields between [...] are optional):

• CP is a (possibly empty) complex argument property ( complex_arg_property/1) which applies to the calls to the predicate.
• CO is a comment string ( docstring/1). This comment only applies if the (possibly empty) properties given for calls in the assertion hold. The usual formatting commands that are applicable in comment strings can be used (see stringcommand/1).

The format of the different parts of the assertion body are given by n_assrt_body/5 and its auxiliary types.

Usage: c_assrt_body(X)

• Description: X is a call assertion body.

REGTYPE: s_assrt_body/1:

This predicate defines the different types of syntax admissible in the bodies of pred/1, func/1, etc. assertions. The following are admissible:

      Pr : CP => AP # CO       
      Pr : CP => AP            
      Pr => AP # CO            
      Pr => AP                 

where:

• Pr is a head pattern ( head_pattern/1) which describes the predicate or property and possibly gives some implicit call/answer information.
• CP is a (possibly empty) complex argument property ( complex_arg_property/1) which applies to the calls to the predicate.
• AP is a (possibly empty) complex argument property ( complex_arg_property/1) which applies to the answers to the predicate (if the predicate succeeds). These only apply if the (possibly empty) properties given for calls in the assertion hold.
• CO is a comment string ( docstring/1). This comment only applies if the (possibly empty) properties given for calls in the assertion hold. The usual formatting commands that are applicable in comment strings can be used (see stringcommand/1).

The format of the different parts of the assertion body are given by n_assrt_body/5 and its auxiliary types.

Usage: s_assrt_body(X)

• Description: X is a predicate assertion body.

REGTYPE: g_assrt_body/1:

This predicate defines the different types of syntax admissible in the bodies of comp/1 assertions. The following are admissible:

      Pr : CP + GP # CO        
      Pr : CP + GP             
      Pr + GP # CO             
      Pr + GP                  

where:

• Pr is a head pattern ( head_pattern/1) which describes the predicate or property and possibly gives some implicit call/answer information.
• CP is a (possibly empty) complex argument property ( complex_arg_property/1) which applies to the calls to the predicate.
• GP contains (possibly empty) complex goal property ( complex_goal_property/1) which applies to the whole execution of a call to the predicate. These only apply if the (possibly empty) properties given for calls in the assertion hold.
• CO is a comment string ( docstring/1). This comment only applies if the (possibly empty) properties given for calls in the assertion hold. The usual formatting commands that are applicable in comment strings can be used (see stringcommand/1).

The format of the different parts of the assertion body are given by n_assrt_body/5 and its auxiliary types.

Usage: g_assrt_body(X)

• Description: X is a comp assertion body.

REGTYPE: assrt_status/1:

The types of assertion status. They have the same meaning as the program-point assertions, and are as follows:

assrt_status(true).
assrt_status(false).
assrt_status(check).
assrt_status(checked).
assrt_status(trust).

Usage: assrt_status(X)

• Description: X is an acceptable status for an assertion.

REGTYPE: assrt_type/1:

The admissible kinds of assertions:

assrt_type(pred).
assrt_type(prop).
assrt_type(decl).
assrt_type(func).
assrt_type(calls).
assrt_type(success).
assrt_type(comp).
assrt_type(entry).
assrt_type(modedef).

Usage: assrt_type(X)

• Description: X is an admissible kind of assertion.

REGTYPE: predfunctor/1:

Usage: predfunctor(X)

• Description: X is a type of assertion which defines a predicate.

REGTYPE: propfunctor/1:

Usage: propfunctor(X)

• Description: X is a type of assertion which defines a property.

PROPERTY: docstring/1:

Usage: docstring(String)

• Description: String is a text comment with admissible documentation commands. The usual formatting commands that are applicable in comment strings are defined by stringcommand/1. See the lpdoc manual for documentation on comments.

Go to the first, previous, next, last section, table of contents.