<HTML>
<HEAD>
<!-- Created by texi2html 1.56k + clip patches and <A href="http://www.clip.dia.fi.upm.es/Software">lpdoc</A> from ciao.texi on 28 January 2007 -->
<LINK rel="stylesheet" href="ciao.css" type="text/css">
<TITLE>The Ciao Prolog System - The Ciao assertion package</TITLE>
</HEAD>
<BODY>
Go to the <A HREF="ciao_1.html">first</A>, <A HREF="ciao_58.html">previous</A>, <A HREF="ciao_60.html">next</A>, <A HREF="ciao_241.html">last</A> section, <A HREF="ciao_toc.html">table of contents</A>.
<P><HR><P>
<H1><A NAME="SEC266" HREF="ciao_toc.html#TOC266">The Ciao assertion package</A></H1>
<P>
<A NAME="IDX3652"></A>
<P>
<STRONG>Author(s):</STRONG> Manuel Hermenegildo, Francisco Bueno, German Puebla.
<P>
<STRONG>Version:</STRONG> 1.10#7 (2006/4/26, 19:22:13 CEST)
<P>
<STRONG>Version of last change:</STRONG> 1.5#8 (1999/12/9, 21:1:11 MET)
<P>
The
<A NAME="IDX3653"></A>
<CODE>assertions</CODE> package adds a number of new declaration definitions and new operator definitions which allow including
<A NAME="IDX3654"></A>
program assertions in user programs. Such assertions can be used to describe predicates, properties, modules, applications, etc. These descriptions can be formal specifications (such as preconditions and post-conditions) or machine-readable textual comments.
<P>
This module is part of the
<A NAME="IDX3655"></A>
<CODE>assertions</CODE> library. It defines the basic code-related assertions, i.e., those intended to be used mainly by compilation-related tools, such as the static analyzer or the run-time test generator.
<P>
Giving
<A NAME="IDX3656"></A>
specifications for predicates and other program elements is the main functionality documented here. The exact syntax of comments
<A NAME="IDX3657"></A>
<A NAME="IDX3658"></A>
is described in the autodocumenter (
<A NAME="IDX3659"></A>
<CODE>lpdoc</CODE> [Knu84,Her99]) manual, although some support for adding machine-readable comments in assertions is also mentioned here.
<P>
There are two kinds of assertions: predicate assertions and program point assertions. All predicate assertions are currently placed as directives in the source code, i.e., preceded by "<CODE>:-</CODE>". Program point assertions are placed as goals in clause bodies.
<UL>
<LI><A HREF="ciao_59.html#SEC267">More info</A>
<LI><A HREF="ciao_59.html#SEC268">Some attention points</A>
<LI><A HREF="ciao_59.html#SEC269">Usage and interface (assertions)</A>
<LI><A HREF="ciao_59.html#SEC270">Documentation on new declarations (assertions)</A>
<LI><A HREF="ciao_59.html#SEC271">Documentation on exports (assertions)</A>
</UL>
<H2><A NAME="SEC267" HREF="ciao_toc.html#TOC267">More info</A></H2>
<P>
The facilities provided by the library are documented in the description of its component modules. This documentation is intended to provide information only at a "reference manual" level. For a more tutorial introduction to the subject and some more examples please see the document "An Assertion Language for Debugging of Constraint Logic Programs (Technical Report CLIP2/97.1)". The assertion language implemented in this library is modeled after this design document, although, due to implementation issues, it may differ in some details. The purpose of this manual is to document precisely what the implementation of the library supports at any given point in time.
<H2><A NAME="SEC268" HREF="ciao_toc.html#TOC268">Some attention points</A></H2>
<UL>
<LI><STRONG>Formatting commands within text strings:</STRONG>
<A NAME="IDX3660"></A>
<A NAME="IDX3661"></A>
many of the predicates defined in these modules include arguments intended for providing textual information. This includes titles, descriptions, comments, etc. The type of this argument is a character string. In order for the automatic generation of documentation to work correctly, this
<A NAME="IDX3662"></A>
character string should adhere to certain conventions. See the description of the
<A NAME="IDX3663"></A>
<CODE>docstring/1</CODE> type/grammar for details.
<LI><STRONG>Referring to variables:</STRONG> In order for the automatic documentation system to work correctly,
<A NAME="IDX3664"></A>
variable names (for example, when referring to arguments in the head patterns of <EM>pred</EM> declarations) must be surrounded by an <CODE>@var</CODE> command. For example, <CODE>@var{VariableName}</CODE> should be used for referring to the variable "VariableName", which will appear then formatted as follows: <CODE>VariableName</CODE>. See the description of the
<A NAME="IDX3665"></A>
<CODE>docstring/1</CODE> type/grammar for details.
</UL>
<H2><A NAME="SEC269" HREF="ciao_toc.html#TOC269">Usage and interface (<CODE>assertions</CODE>)</A></H2>
<div class="cartouche">
<UL>
<LI><STRONG>Library usage:</STRONG>
The recommended procedure in order to make use of assertions in user programs is to include the
<A NAME="IDX3666"></A>
<CODE>assertions</CODE> syntax library, using one of the following declarations, as appropriate:
<PRE>
:- module(...,...,[assertions]).
:- include(library(assertions)).
:- use_package([assertions]).
</PRE>
<LI><STRONG>Exports:</STRONG>
<UL>
<LI><EM>Predicates:</EM>
<A NAME="IDX3667"></A>
<CODE>check/1</CODE>,
<A NAME="IDX3668"></A>
<CODE>trust/1</CODE>,
<A NAME="IDX3669"></A>
<CODE>true/1</CODE>,
<A NAME="IDX3670"></A>
<CODE>false/1</CODE>.
</UL>
<LI><STRONG>New operators defined:</STRONG>
<A NAME="IDX3671"></A>
<CODE>=>/2</CODE> [975,xfx],
<A NAME="IDX3672"></A>
<CODE>::/2</CODE> [978,xfx],
<A NAME="IDX3673"></A>
<CODE>decl/1</CODE> [1150,fx],
<A NAME="IDX3674"></A>
<CODE>decl/2</CODE> [1150,xfx],
<A NAME="IDX3675"></A>
<CODE>pred/1</CODE> [1150,fx],
<A NAME="IDX3676"></A>
<CODE>pred/2</CODE> [1150,xfx],
<A NAME="IDX3677"></A>
<CODE>prop/1</CODE> [1150,fx],
<A NAME="IDX3678"></A>
<CODE>prop/2</CODE> [1150,xfx],
<A NAME="IDX3679"></A>
<CODE>modedef/1</CODE> [1150,fx],
<A NAME="IDX3680"></A>
<CODE>calls/1</CODE> [1150,fx],
<A NAME="IDX3681"></A>
<CODE>calls/2</CODE> [1150,xfx],
<A NAME="IDX3682"></A>
<CODE>success/1</CODE> [1150,fx],
<A NAME="IDX3683"></A>
<CODE>success/2</CODE> [1150,xfx],
<A NAME="IDX3684"></A>
<CODE>comp/1</CODE> [1150,fx],
<A NAME="IDX3685"></A>
<CODE>comp/2</CODE> [1150,xfx],
<A NAME="IDX3686"></A>
<CODE>entry/1</CODE> [1150,fx].
<LI><STRONG>New declarations defined:</STRONG>
<A NAME="IDX3687"></A>
<CODE>pred/1</CODE>,
<A NAME="IDX3688"></A>
<CODE>pred/2</CODE>,
<A NAME="IDX3689"></A>
<CODE>calls/1</CODE>,
<A NAME="IDX3690"></A>
<CODE>calls/2</CODE>,
<A NAME="IDX3691"></A>
<CODE>success/1</CODE>,
<A NAME="IDX3692"></A>
<CODE>success/2</CODE>,
<A NAME="IDX3693"></A>
<CODE>comp/1</CODE>,
<A NAME="IDX3694"></A>
<CODE>comp/2</CODE>,
<A NAME="IDX3695"></A>
<CODE>prop/1</CODE>,
<A NAME="IDX3696"></A>
<CODE>prop/2</CODE>,
<A NAME="IDX3697"></A>
<CODE>entry/1</CODE>,
<A NAME="IDX3698"></A>
<CODE>modedef/1</CODE>,
<A NAME="IDX3699"></A>
<CODE>decl/1</CODE>,
<A NAME="IDX3700"></A>
<CODE>decl/2</CODE>,
<A NAME="IDX3701"></A>
<CODE>comment/2</CODE>.
<LI><STRONG>Other modules used:</STRONG>
<UL>
<LI><EM>System library modules:</EM>
<A NAME="IDX3702"></A>
<CODE>assertions/assertions_props</CODE>.
</UL>
</UL>
</div class="cartouche">
<H2><A NAME="SEC270" HREF="ciao_toc.html#TOC270">Documentation on new declarations (<CODE>assertions</CODE>)</A></H2>
<P>
<A NAME="IDX3703"></A>
<A NAME="IDX3704"></A>
<DL>
<DT><span class="define">DECLARATION:</span> <B>pred/1:</B>
<DD><A NAME="IDX3705"></A>
<P>
<A NAME="IDX3706"></A>
<A NAME="IDX3707"></A>
This assertion provides information on a predicate. The body of the assertion (its only argument) contains properties or comments in the formats defined by
<A NAME="IDX3708"></A>
<CODE>assrt_body/1</CODE>.
<P>
More than one of these assertions may appear per predicate, in which case each one represents a possible "
<A NAME="IDX3709"></A>
mode" of use (
<A NAME="IDX3710"></A>
usage) of the predicate. The exact scope of the usage is defined by the properties given for calls in the body of each assertion (which should thus distinguish the different usages intended). All of them together cover all possible modes of usage.
<P>
For example, the following assertions describe (all the and the only) modes of usage of predicate <CODE>length/2</CODE> (see
<A NAME="IDX3711"></A>
<CODE>lists</CODE>):
<PRE>
:- pred length(L,N) : list * var => list * integer
# "Computes the length of <CODE>L</CODE>.".
:- pred length(L,N) : var * integer => list * integer
# "Outputs <CODE>L</CODE> of length <CODE>N</CODE>.".
:- pred length(L,N) : list * integer => list * integer
# "Checks that <CODE>L</CODE> is of length <CODE>N</CODE>.".
</PRE>
<P>
<STRONG>Usage:</STRONG> :- <CODE>pred(AssertionBody)</CODE>.
<UL>
<LI><EM>The following properties should hold at call time:</EM>
<CODE>AssertionBody</CODE> is an assertion body.
(<CODE>assertions_props:assrt_body/1</CODE>)
</UL>
</DL>
<P>
<A NAME="IDX3712"></A>
<A NAME="IDX3713"></A>
<DL>
<DT><span class="define">DECLARATION:</span> <B>pred/2:</B>
<DD><A NAME="IDX3714"></A>
<P>
<A NAME="IDX3715"></A>
<A NAME="IDX3716"></A>
This assertion is similar to a
<A NAME="IDX3717"></A>
<CODE>pred/1</CODE> assertion but it is explicitely qualified. Non-qualified
<A NAME="IDX3718"></A>
<CODE>pred/1</CODE> assertions are assumed the qualifier <CODE>check</CODE>.
<P>
<STRONG>Usage:</STRONG> :- <CODE>pred(AssertionStatus, AssertionBody)</CODE>.
<UL>
<LI><EM>The following properties should hold at call time:</EM>
<CODE>AssertionStatus</CODE> is an acceptable status for an assertion.
(<CODE>assertions_props:assrt_status/1</CODE>)
<CODE>AssertionBody</CODE> is an assertion body.
(<CODE>assertions_props:assrt_body/1</CODE>)
</UL>
</DL>
<P>
<A NAME="IDX3719"></A>
<A NAME="IDX3720"></A>
<DL>
<DT><span class="define">DECLARATION:</span> <B>calls/1:</B>
<DD><A NAME="IDX3721"></A>
<P>
<A NAME="IDX3722"></A>
<A NAME="IDX3723"></A>
This assertion is similar to a
<A NAME="IDX3724"></A>
<CODE>pred/1</CODE> assertion but it only provides information about the calls to a predicate. If one or several calls assertions are given they are understood to describe all possible calls to the predicate.
<P>
For example, the following assertion describes all possible calls to predicate <CODE>is/2</CODE> (see
<A NAME="IDX3725"></A>
<CODE>arithmetic</CODE>):
<PRE>
:- calls is(term,arithexpression).
</PRE>
<P>
<STRONG>Usage:</STRONG> :- <CODE>calls(AssertionBody)</CODE>.
<UL>
<LI><EM>The following properties should hold at call time:</EM>
<CODE>AssertionBody</CODE> is a call assertion body.
(<CODE>assertions_props:c_assrt_body/1</CODE>)
</UL>
</DL>
<P>
<A NAME="IDX3726"></A>
<A NAME="IDX3727"></A>
<DL>
<DT><span class="define">DECLARATION:</span> <B>calls/2:</B>
<DD><A NAME="IDX3728"></A>
<P>
<A NAME="IDX3729"></A>
<A NAME="IDX3730"></A>
This assertion is similar to a
<A NAME="IDX3731"></A>
<CODE>calls/1</CODE> assertion but it is explicitely qualified. Non-qualified
<A NAME="IDX3732"></A>
<CODE>calls/1</CODE> assertions are assumed the qualifier <CODE>check</CODE>.
<P>
<STRONG>Usage:</STRONG> :- <CODE>calls(AssertionStatus, AssertionBody)</CODE>.
<UL>
<LI><EM>The following properties should hold at call time:</EM>
<CODE>AssertionStatus</CODE> is an acceptable status for an assertion.
(<CODE>assertions_props:assrt_status/1</CODE>)
<CODE>AssertionBody</CODE> is a call assertion body.
(<CODE>assertions_props:c_assrt_body/1</CODE>)
</UL>
</DL>
<P>
<A NAME="IDX3733"></A>
<A NAME="IDX3734"></A>
<DL>
<DT><span class="define">DECLARATION:</span> <B>success/1:</B>
<DD><A NAME="IDX3735"></A>
<P>
<A NAME="IDX3736"></A>
<A NAME="IDX3737"></A>
This assertion is similar to a
<A NAME="IDX3738"></A>
<CODE>pred/1</CODE> assertion but it only provides information about the answers to a predicate. The described answers might be conditioned to a particular way of calling the predicate.
<P>
For example, the following assertion specifies the answers of the <CODE>length/2</CODE> predicate <EM>if</EM> it is called as in the first mode of usage above (note that the previous pred assertion already conveys such information, however it also compelled the predicate calls, while the success assertion does not):
<PRE>
:- success length(L,N) : list * var => list * integer.
</PRE>
<P>
<STRONG>Usage:</STRONG> :- <CODE>success(AssertionBody)</CODE>.
<UL>
<LI><EM>The following properties should hold at call time:</EM>
<CODE>AssertionBody</CODE> is a predicate assertion body.
(<CODE>assertions_props:s_assrt_body/1</CODE>)
</UL>
</DL>
<P>
<A NAME="IDX3739"></A>
<A NAME="IDX3740"></A>
<DL>
<DT><span class="define">DECLARATION:</span> <B>success/2:</B>
<DD><A NAME="IDX3741"></A>
<P>
<A NAME="IDX3742"></A>
<A NAME="IDX3743"></A>
This assertion is similar to a
<A NAME="IDX3744"></A>
<CODE>success/1</CODE> assertion but it is explicitely qualified. Non-qualified
<A NAME="IDX3745"></A>
<CODE>success/1</CODE> assertions are assumed the qualifier <CODE>check</CODE>.
<P>
<STRONG>Usage:</STRONG> :- <CODE>success(AssertionStatus, AssertionBody)</CODE>.
<UL>
<LI><EM>The following properties should hold at call time:</EM>
<CODE>AssertionStatus</CODE> is an acceptable status for an assertion.
(<CODE>assertions_props:assrt_status/1</CODE>)
<CODE>AssertionBody</CODE> is a predicate assertion body.
(<CODE>assertions_props:s_assrt_body/1</CODE>)
</UL>
</DL>
<P>
<A NAME="IDX3746"></A>
<A NAME="IDX3747"></A>
<DL>
<DT><span class="define">DECLARATION:</span> <B>comp/1:</B>
<DD><A NAME="IDX3748"></A>
<P>
<A NAME="IDX3749"></A>
<A NAME="IDX3750"></A>
This assertion is similar to a
<A NAME="IDX3751"></A>
<CODE>pred/1</CODE> assertion but it only provides information about the global execution properties of a predicate (note that such kind of information is also conveyed by pred assertions). The described properties might be conditioned to a particular way of calling the predicate.
<P>
For example, the following assertion specifies that the computation of <CODE>append/3</CODE> (see
<A NAME="IDX3752"></A>
<CODE>lists</CODE>) will not fail <EM>if</EM> it is called as described (but does not compel the predicate to be called that way):
<PRE>
:- comp append(Xs,Ys,Zs) : var * var * var + not_fail.
</PRE>
<P>
<STRONG>Usage:</STRONG> :- <CODE>comp(AssertionBody)</CODE>.
<UL>
<LI><EM>The following properties should hold at call time:</EM>
<CODE>AssertionBody</CODE> is a comp assertion body.
(<CODE>assertions_props:g_assrt_body/1</CODE>)
</UL>
</DL>
<P>
<A NAME="IDX3753"></A>
<A NAME="IDX3754"></A>
<DL>
<DT><span class="define">DECLARATION:</span> <B>comp/2:</B>
<DD><A NAME="IDX3755"></A>
<P>
<A NAME="IDX3756"></A>
<A NAME="IDX3757"></A>
This assertion is similar to a
<A NAME="IDX3758"></A>
<CODE>comp/1</CODE> assertion but it is explicitely qualified. Non-qualified
<A NAME="IDX3759"></A>
<CODE>comp/1</CODE> assertions are assumed the qualifier <CODE>check</CODE>.
<P>
<STRONG>Usage:</STRONG> :- <CODE>comp(AssertionStatus, AssertionBody)</CODE>.
<UL>
<LI><EM>The following properties should hold at call time:</EM>
<CODE>AssertionStatus</CODE> is an acceptable status for an assertion.
(<CODE>assertions_props:assrt_status/1</CODE>)
<CODE>AssertionBody</CODE> is a comp assertion body.
(<CODE>assertions_props:g_assrt_body/1</CODE>)
</UL>
</DL>
<P>
<A NAME="IDX3760"></A>
<A NAME="IDX3761"></A>
<DL>
<DT><span class="define">DECLARATION:</span> <B>prop/1:</B>
<DD><A NAME="IDX3762"></A>
<P>
<A NAME="IDX3763"></A>
<A NAME="IDX3764"></A>
This assertion is similar to a <CODE>pred/1</CODE> assertion but it flags that the predicate being documented is also a "
<A NAME="IDX3765"></A>
property."
<P>
Properties are standard predicates, but which are <EM>guaranteed to terminate for any possible instantiation state of their argument(s)</EM>, do not perform side-effects which may interfere with the program behaviour, and do not further instantiate their arguments or add new constraints.
<P>
Provided the above holds, properties can thus be safely used as
<A NAME="IDX3766"></A>
run-time checks. The program transformation used in <CODE>ciaopp</CODE> for run-time checking guarantees the third requirement. It also performs some basic checks on properties which in most cases are enough for the second requirement. However, it is the user's responsibility to guarantee termination of the properties defined. (See also section <A HREF="ciao_61.html#SEC275">Declaring regular types</A> for some considerations applicable to writing properties.)
<P>
The set of properties is thus a strict subset of the set of predicates. Note that properties can be used to describe characteristics of arguments in assertions and they can also be executed (called) as any other predicates.
<P>
<STRONG>Usage:</STRONG> :- <CODE>prop(AssertionBody)</CODE>.
<UL>
<LI><EM>The following properties should hold at call time:</EM>
<CODE>AssertionBody</CODE> is an assertion body.
(<CODE>assertions_props:assrt_body/1</CODE>)
</UL>
</DL>
<P>
<A NAME="IDX3767"></A>
<A NAME="IDX3768"></A>
<DL>
<DT><span class="define">DECLARATION:</span> <B>prop/2:</B>
<DD><A NAME="IDX3769"></A>
<P>
<A NAME="IDX3770"></A>
<A NAME="IDX3771"></A>
This assertion is similar to a
<A NAME="IDX3772"></A>
<CODE>prop/1</CODE> assertion but it is explicitely qualified. Non-qualified
<A NAME="IDX3773"></A>
<CODE>prop/1</CODE> assertions are assumed the qualifier <CODE>check</CODE>.
<P>
<STRONG>Usage:</STRONG> :- <CODE>prop(AssertionStatus, AssertionBody)</CODE>.
<UL>
<LI><EM>The following properties should hold at call time:</EM>
<CODE>AssertionStatus</CODE> is an acceptable status for an assertion.
(<CODE>assertions_props:assrt_status/1</CODE>)
<CODE>AssertionBody</CODE> is an assertion body.
(<CODE>assertions_props:assrt_body/1</CODE>)
</UL>
</DL>
<P>
<A NAME="IDX3774"></A>
<A NAME="IDX3775"></A>
<DL>
<DT><span class="define">DECLARATION:</span> <B>entry/1:</B>
<DD><A NAME="IDX3776"></A>
<P>
<A NAME="IDX3777"></A>
<A NAME="IDX3778"></A>
This assertion provides information about the <EM>external</EM> calls to a predicate. It is identical syntactically to a
<A NAME="IDX3779"></A>
<CODE>calls/1</CODE> assertion. However, they describe only external calls, i.e., calls to the exported predicates of a module from outside the module, or calls to the predicates in a non-modular file from other files (or the user).
<P>
These assertions are <EM>trusted</EM> by the compiler. As a result, if their descriptions are erroneous they can introduce bugs in programs. Thus,
<A NAME="IDX3780"></A>
<CODE>entry/1</CODE> assertions should be written with care.
<P>
An important use of these assertions is in
<A NAME="IDX3781"></A>
providing information to the compiler which it may not be able to infer from the program. The main use is in providing information on the ways in which exported predicates of a module will be called from outside the module. This will greatly improve the precision of the analyzer, which otherwise has to assume that the arguments that exported predicates receive are any arbitrary term.
<P>
<STRONG>Usage:</STRONG> :- <CODE>entry(AssertionBody)</CODE>.
<UL>
<LI><EM>The following properties should hold at call time:</EM>
<CODE>AssertionBody</CODE> is a call assertion body.
(<CODE>assertions_props:c_assrt_body/1</CODE>)
</UL>
</DL>
<P>
<A NAME="IDX3782"></A>
<A NAME="IDX3783"></A>
<DL>
<DT><span class="define">DECLARATION:</span> <B>modedef/1:</B>
<DD><A NAME="IDX3784"></A>
<P>
This assertion is used to define modes. A mode defines in a compact way a set of call and success properties. Once defined, modes can be applied to predicate arguments in assertions. The meaning of this application is that the call and success properties defined by the mode hold for the argument to which the mode is applied. Thus, a mode is conceptually a "property macro".
<P>
The syntax of mode definitions is similar to that of pred declarations. For example, the following set of assertions:
<PRE>
:- modedef +A : nonvar(A) # "<CODE>A</CODE> is bound upon predicate entry.".
:- pred p(+A,B) : integer(A) => ground(B).
</PRE>
<P>
is equivalent to:
<PRE>
:- pred p(A,B) : (nonvar(A),integer(A)) => ground(B)
# "<CODE>A</CODE> is bound upon predicate entry.".
</PRE>
<P>
<STRONG>Usage:</STRONG> :- <CODE>modedef(AssertionBody)</CODE>.
<UL>
<LI><EM>The following properties should hold at call time:</EM>
<CODE>AssertionBody</CODE> is an assertion body.
(<CODE>assertions_props:assrt_body/1</CODE>)
</UL>
</DL>
<P>
<A NAME="IDX3785"></A>
<A NAME="IDX3786"></A>
<DL>
<DT><span class="define">DECLARATION:</span> <B>decl/1:</B>
<DD><A NAME="IDX3787"></A>
<P>
<A NAME="IDX3788"></A>
<A NAME="IDX3789"></A>
This assertion is similar to a
<A NAME="IDX3790"></A>
<CODE>pred/1</CODE> assertion but it is used for declarations instead than for predicates.
<P>
<STRONG>Usage:</STRONG> :- <CODE>decl(AssertionBody)</CODE>.
<UL>
<LI><EM>The following properties should hold at call time:</EM>
<CODE>AssertionBody</CODE> is an assertion body.
(<CODE>assertions_props:assrt_body/1</CODE>)
</UL>
</DL>
<P>
<A NAME="IDX3791"></A>
<A NAME="IDX3792"></A>
<DL>
<DT><span class="define">DECLARATION:</span> <B>decl/2:</B>
<DD><A NAME="IDX3793"></A>
<P>
<A NAME="IDX3794"></A>
<A NAME="IDX3795"></A>
This assertion is similar to a
<A NAME="IDX3796"></A>
<CODE>decl/1</CODE> assertion but it is explicitely qualified. Non-qualified
<A NAME="IDX3797"></A>
<CODE>decl/1</CODE> assertions are assumed the qualifier <CODE>check</CODE>.
<P>
<STRONG>Usage:</STRONG> :- <CODE>decl(AssertionStatus, AssertionBody)</CODE>.
<UL>
<LI><EM>The following properties should hold at call time:</EM>
<CODE>AssertionStatus</CODE> is an acceptable status for an assertion.
(<CODE>assertions_props:assrt_status/1</CODE>)
<CODE>AssertionBody</CODE> is an assertion body.
(<CODE>assertions_props:assrt_body/1</CODE>)
</UL>
</DL>
<P>
<A NAME="IDX3798"></A>
<A NAME="IDX3799"></A>
<DL>
<DT><span class="define">DECLARATION:</span> <B>comment/2:</B>
<DD><A NAME="IDX3800"></A>
<P>
<STRONG>Usage:</STRONG> :- <CODE>comment(Pred, Comment)</CODE>.
<UL>
<LI><EM>Description:</EM>
<A NAME="IDX3801"></A>
<A NAME="IDX3802"></A>
This assertion gives a text <CODE>Comment</CODE> for a given predicate <CODE>Pred</CODE>.
<LI><EM>The following properties should hold at call time:</EM>
<CODE>Pred</CODE> is a head pattern.
(<CODE>assertions_props:head_pattern/1</CODE>)
<CODE>Comment</CODE> is a text comment with admissible documentation commands. The usual formatting commands that are applicable in comment strings are defined by
<A NAME="IDX3803"></A>
<CODE>stringcommand/1</CODE>. See the
<A NAME="IDX3804"></A>
<CODE>lpdoc</CODE> manual for documentation on comments.
(<CODE>assertions_props:docstring/1</CODE>)
</UL>
</DL>
<H2><A NAME="SEC271" HREF="ciao_toc.html#TOC271">Documentation on exports (<CODE>assertions</CODE>)</A></H2>
<P>
<A NAME="IDX3805"></A>
<A NAME="IDX3806"></A>
<DL>
<DT><span class="define">PREDICATE:</span> <B>check/1:</B>
<DD><A NAME="IDX3807"></A>
<P>
<STRONG>Usage:</STRONG> <CODE>check(PropertyConjunction)</CODE>
<UL>
<LI><EM>Description:</EM>
<A NAME="IDX3808"></A>
<A NAME="IDX3809"></A>
This assertion provides information on a clause program point (position in the body of a clause). Calls to a
<A NAME="IDX3810"></A>
<CODE>check/1</CODE> assertion can appear in the body of a clause in any place where a literal can normally appear. The property defined by <CODE>PropertyConjunction</CODE> should hold in all the run-time stores corresponding to that program point. See also section <A HREF="ciao_65.html#SEC288">Run-time checking of assertions</A>.
<LI><EM>The following properties should hold at call time:</EM>
<CODE>PropertyConjunction</CODE> is either a term or a <EM>conjunction</EM> 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.
(<CODE>assertions_props:property_conjunction/1</CODE>)
</UL>
</DL>
<P>
<A NAME="IDX3811"></A>
<A NAME="IDX3812"></A>
<DL>
<DT><span class="define">PREDICATE:</span> <B>trust/1:</B>
<DD><A NAME="IDX3813"></A>
<P>
<STRONG>Usage:</STRONG> <CODE>trust(PropertyConjunction)</CODE>
<UL>
<LI><EM>Description:</EM>
<A NAME="IDX3814"></A>
<A NAME="IDX3815"></A>
This assertion also provides information on a clause program point. It is identical syntactically to a
<A NAME="IDX3816"></A>
<CODE>check/1</CODE> assertion. However, the properties stated are not taken as something to be checked but are instead <EM>trusted</EM> by the compiler. While the compiler may in some cases detect an inconsistency between a
<A NAME="IDX3817"></A>
<CODE>trust/1</CODE> assertion and the program, in all other cases the information given in the assertion will be taken to be true. As a result, if these assertions are erroneous they can introduce bugs in programs. Thus,
<A NAME="IDX3818"></A>
<CODE>trust/1</CODE> assertions should be written with care.
An important use of these assertions is in
<A NAME="IDX3819"></A>
providing information to the compiler which it may not be able to infer from the program (either because the information is not present or because the analyzer being used is not precise enough). In particular, providing information on external predicates which may not be accessible at the time of compiling the module can greatly improve the precision of the analyzer. This can be easily done with trust assertion.
<LI><EM>The following properties should hold at call time:</EM>
<CODE>PropertyConjunction</CODE> is either a term or a <EM>conjunction</EM> 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.
(<CODE>assertions_props:property_conjunction/1</CODE>)
</UL>
</DL>
<P>
<A NAME="IDX3820"></A>
<A NAME="IDX3821"></A>
<DL>
<DT><span class="define">PREDICATE:</span> <B>true/1:</B>
<DD><A NAME="IDX3822"></A>
<P>
<STRONG>Usage:</STRONG> <CODE>true(PropertyConjunction)</CODE>
<UL>
<LI><EM>Description:</EM>
<A NAME="IDX3823"></A>
<A NAME="IDX3824"></A>
This assertion is identical syntactically to a
<A NAME="IDX3825"></A>
<CODE>check/1</CODE> assertion. However, the properties stated have been proved to hold by the analyzer. Thus, these assertions often represent the
<A NAME="IDX3826"></A>
analyzer output.
<LI><EM>The following properties should hold at call time:</EM>
<CODE>PropertyConjunction</CODE> is either a term or a <EM>conjunction</EM> 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.
(<CODE>assertions_props:property_conjunction/1</CODE>)
</UL>
</DL>
<P>
<A NAME="IDX3827"></A>
<A NAME="IDX3828"></A>
<DL>
<DT><span class="define">PREDICATE:</span> <B>false/1:</B>
<DD><A NAME="IDX3829"></A>
<P>
<STRONG>Usage:</STRONG> <CODE>false(PropertyConjunction)</CODE>
<UL>
<LI><EM>Description:</EM>
<A NAME="IDX3830"></A>
<A NAME="IDX3831"></A>
This assertion is identical syntactically to a
<A NAME="IDX3832"></A>
<CODE>check/1</CODE> assertion. However, the properties stated have been proved not to hold by the analyzer. Thus, these assertions often represent the
<A NAME="IDX3833"></A>
analyzer output.
<LI><EM>The following properties should hold at call time:</EM>
<CODE>PropertyConjunction</CODE> is either a term or a <EM>conjunction</EM> 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.
(<CODE>assertions_props:property_conjunction/1</CODE>)
</UL>
</DL>
<P><HR><P>
Go to the <A HREF="ciao_1.html">first</A>, <A HREF="ciao_58.html">previous</A>, <A HREF="ciao_60.html">next</A>, <A HREF="ciao_241.html">last</A> section, <A HREF="ciao_toc.html">table of contents</A>.
</BODY>
</HTML>
