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

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)