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

 before(Arg1)

 after(Arg1)

 init_expansors