|Did you know ...||Search Documentation:|
|Pack assertions -- prolog/assertions.pl|
@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
assrt_meta.plfor an example). The first argument is wrapped to facilitate indexing. Note that it is recommended that multiple clauses of this predicate be mutually exclusive.
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
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).
The following predicates are exported, but not or incorrectly documented.