Not an ISO Standard exception
assertion/1 throws a non-ISO Standard error term
there is no ISO standard assertion error ... hard to believe!
An assertion exception is special somehow
Interactively, it doesn't seem to be "catchable" with catch/3 (compare with Java where an "Throwable" is not caught if you just catch its subclass "Exceptions")
This even if
set_prolog_flag(debug_on_error,false) has been set.
A domain error is not a problem:
?- catch(domain_error(_,_),Caught,format("Caught: ~q~n",[Caught])). Caught: error(domain_error(_96,_98),_92) Caught = error(domain_error(_96,_98),_92).
But an assertion error goes right through and starts the tracer:
?- catch(assertion(false),Caught,format("Caught: ~q~n",[Caught])). ERROR: Assertion failed: user:false  prolog_stack: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:330  prolog_debug:assertion(user:false) at /usr/local/logic/swipl/lib/swipl/library/debug.pl:318  catch(user:assertion(false),_2174,user:format("Caught: ~q~n",...)) at /usr/local/logic/swipl/lib/swipl/boot/init.pl:537  toplevel_call(user:user: ...) at /usr/local/logic/swipl/lib/swipl/boot/toplevel.pl:1113 true.
If you have this program:
main :- catch(domain_error(_,_),Caught,format("Caught: ~q~n",[Caught])), format("Next...~n",), catch(assertion(false),Caught,format("Caught: ~q~n",[Caught])), format("There is no next...~n",). :- main.
and run it:
$ swipl test.pl Caught: error(domain_error(_41980,_41982),_41976) Next... ERROR: /home/user/test.pl:7: ERROR: Assertion failed: user:false  prolog_stack: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:330 ...
assertion does not backtrack and has no effects
Sounds like it deploys a "double negation" firewall. Good:
?- assertion(member(X,[1,2,3])), % this passes format("~q",[X]). % but X is still uninstantiated _84182 true.
- The assertion-handling source is in
- The message printing source is in
lib/swipl/boot/messages.plThe assertion-handling source is a bit esoteric but we see the double negation here:
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').
When to use this?
Answer: All the time.
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.
On the other hand, in my opinion must_be/2 is much too rigid (i.e. the approach is very C-like). It is able to perform a selected number of relatively basic type checks, whereas you can give an arbitrary goal to assertion/1 and go wild with the conditions while staying readable.
- An ability to disable assertion/1 for a subgoals, similarl to the way you redirect current output for subgolas with with_output_to/2.
- Assertions should be categorized by a term, similar to logging, so that one can switch them off or on in groups. Of course, this could be done writing the assertion/1 subgoal adequately but that is icky.
- There should be an optional error message. If Java accepts an error message in its assert statement there must be a reason for that. However, after querying, this is not planned to be added.
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.
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."
Prolog is worse off with is arbitrary dataflow and lack of static and strong typing. Deploy assertions to keep it in line.
Non-Prolog related reading
A historical perspective on runtime assertion checking in software development , Lori A. Clarke, David S. Rosenblum, 2006.
- 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: Very well. One body with multiple tests using assertions. In fact, I prefer to use assertion/1 calls in plunit tests rather than plunit-style tests in the header, they are much more readable & flexible.