Did you know ... Search Documentation:
Pack assertions -- prolog/assertions.pl
PublicShow source

@note: asr_* declared multifile to allow extensibility. At this point you extend concrete assertions (not abstractions or fake ones, since they will be collected by the run-time checker, for instance)

@note: Next syntax is ambiguous, but shorter:

  :- det callable.

is equivalent to:

  :- true prop callable/1 is det

but can be confused with:

:- true prop det(callable)
:- true prop det(X) :: callable(X).

in any case this is syntax sugar so we can always write the long version of the assertion to avoid ambiguities

 asr_head(?Asr, ?Head) is det
Extract the Head for a given assertion identifier. Note that the first and second arguments of the Assertion identifier should contain the module and the head respectively.
 asr_aprop(+Asr, +Key, ?Prop, -From)[multifile]
Extensible accessor to assertion properties, ideal to have different views of assertions, to extend the assertions or to create ancillary assertions (see module assrt_meta.pl for an example). The first argument is wrapped to facilitate indexing. Note that it is recommended that multiple clauses of this predicate be mutually exclusive.
 assrt_type(Type)
The type of assertion, could have the following values:

calls - Specifies the properties at call time.

success - Specifies the properties on success, but only for external calls.

comp - Assertion type comp, specifies computational or global properties.

prop - States that the predicate is a property

pred - Union of calls, success and comp assertion types

 assrt_status(Status)
The status of an assertion. Be careful, since they are not compatible with those found in Ciao-Prolog. Could have the following values:

check - Assertion should be checked statically or with the rtcheck tracer (default)

true - Assertion is true, provided by the user

false - Assertion is false, provided by the user (not implemented yet)

debug - Assertion should be checked only at development time

static - Assertion is always instrumented in the code via a wrapper, in other words, it is considered part of the implementation.

@note: For static, such instrumentation can be removed only if a static analysis prove it is always true (not implemented yet).

To be done
- : The next are intended to be used internally, once the system be able to infer new assertions:

right: inferred by the static analysis trust: Ciao-Prolog like, provided by the user fail: false, inferred by the static analyss.

 expand_assertion(+Decl, DPos, -Records, RPos) is semidet
Process a Declaration as an assertion. This is called in a term_expansion/2 of the assertion module. Fails if Decl is not a valid assertion.

Undocumented predicates

The following predicates are exported, but not or incorrectly documented.

 asr_head_prop(Arg1, Arg2, Arg3, Arg4, Arg5, Arg6, Arg7, Arg8)
 curr_prop_asr(Arg1, Arg2, Arg3, Arg4)
 aprop_asr(Arg1, Arg2, Arg3, Arg4)
 prop_asr(Arg1, Arg2, Arg3, Arg4)
 prop_asr(Arg1, Arg2, Arg3, Arg4, Arg5, Arg6, Arg7)
 current_decomposed_assertion_1(Arg1, Arg2, Arg3, Arg4, Arg5, Arg6, Arg7, Arg8, Arg9, Arg10, Arg11, Arg12)
 decompose_assertion_head_body(Arg1, Arg2, Arg3, Arg4, Arg5, Arg6, Arg7, Arg8, Arg9, Arg10, Arg11, Arg12, Arg13)