When to use this?
Jan Wielemaker writes:
Public APIs should not use assertion/1 to validate argument types. must_be/2 is intended for this. assertion/1 is intended to trap stuff that should not happen unless there is a bug in the library.
OTOH, in my opinion must_be/2 is too rigid (i.e. very C-like). It is able to perform a selected number of relatively basic type check, whereas you can give a whole goal to assertion/1 and go wild while staying readable.
WISH: The ideal way would be to have a must_be/3 that doesn't throw but just fails with a proper error message on third place. Then you could call that through
assertionx(Key,Goal,Txt) where Key is an atom by which the assertionx/3 can be switched on or off (by consulting the Prolog database, naturally) and Txt is the text to be put into a dedicated assertion error to throw on assertion violation. That would a non-ISO error because there is no ISO standard assertion error ... hard to believe!)
A statistic of interest
Gerard J. Holzmann writes in IEEE Software, January/February 2021 in "Right Code".
"For the mission code that is developed at NASA/Jet Propulsion Laboratory, we require that the average assertion density for each module is 2% or more. This means that 2% of the code performs self-checks at key steps in the computations performed to make sure that integrity is maintained, even in anomalous execution scenarios. The use of assertions thus provides a form of software redundancy that can indeed make a system more reliable."
assertion(false) on the Prolog toplevel directly gives:
?- assertion(false). ERROR: Assertion failed: user:false  backtrace(10) at /usr/local/logic/swipl/lib/swipl/library/prolog_stack.pl:487  prolog_debug:assertion_failed(fail,user:false) at /usr/local/logic/swipl/lib/swipl/library/debug.pl:328  prolog_debug:assertion(user:false) at /usr/local/logic/swipl/lib/swipl/library/debug.pl:316  <user> true. [trace] ?- nodebug. true. ?-
main :- catch_with_backtrace(assertion(false),H,writeln(H)). :- main.
ERROR: /home/user/test.pl:6: ERROR: Assertion failed: user:false  backtrace(10) at ...  prolog_debug:assertion_failed(fail,user:false) at ...  prolog_debug:assertion(user:false) at ...  catch(user:assertion(false),_13924,user:writeln(_13954)) at ...  catch_with_backtrace(user:assertion(false),_14008,user:writeln(_14038)) at ...  main at ...  catch(user:main,error(_14148,_14150),system:'$exception_in_directive'(...)) at ...  '$execute_directive_3'(main) at ...  '$load_file'('/home/calvin/ass2.pl','/home/calvin/ass2.pl',_14270,[expand(false),...]) at ...  setup_call_catcher_cleanup(...
- See also must_be/2
- Here's how CIAO Prolog does it: https://ciao-lang.org/ciao/build/doc/ciao.html/assertions_doc.html
- ... and there is a corresponding package for SWI-Prolog: https://eu.swi-prolog.org/pack/list?p=assertions
- How assertion/1 works together with plunit: One body with multiple tests using assertions
No message text
It might be nice if this predicate also took a second argument (possibly a goal) to generate a text for the exception so as to inform the user in a more detailed fashion concerning the failure. Similar for Java: 14.10. The assert Statement.
However, this is not planned to be added for now.
You need to rewrite them using goal_expansion/2.
For example, load and execute:
:- debug(assertion_info). % --- % plunit test code % --- foo(X) :- bar(X). bar(X) :- baz(X). baz(X) :- quux(X). quux(X) :- assertion(X > 0), debug(assertion_info,"Now past assertion",).
On the command line:
?- [ass]. true. ?- quux(1). % Now past assertion true. ?- quux(-1). ERROR: Assertion failed: user:(-1>0)
Now add this to
goal_expansion(assertion(G),true) :- format("Replaced assertion: ~q\n",[assertion(G)]).
then loading the above program again:
?- [ass]. Replaced assertion: assertion(_20756>0) true. ?- quux(-1). % Now past assertion true. ?- quux(1). % Now past assertion true.
More complex body to goal_expansion/2 will also allow you to disable assertions on a per-module basis for example.
- The assertion-handling source is in
- The message printing source is in
lib/swipl/boot/messages.plThe assertion-handling source is a bit esoteric:
assertion(G) :- \+ \+ catch(G, Error, assertion_failed(Error, G)), !. assertion(G) :- assertion_failed(fail, G), assertion_failed. % prevent last call optimization. assertion_failed(Reason, G) :- prolog:assertion_failed(Reason, G), !. assertion_failed(Reason, _) :- assertion_rethrow(Reason), !, throw(Reason). assertion_failed(Reason, G) :- print_message(error, assertion_failed(Reason, G)), backtrace(10), ( current_prolog_flag(break_level, _) % interactive thread -> trace ; throw(error(assertion_error(Reason, G), _)) ). assertion_failed. assertion_rethrow(time_limit_exceeded). assertion_rethrow('$aborted').