Not an ISO Standard exception
assertion/1 throws a non-ISO Standard error term
because
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 [13] prolog_stack:backtrace(10) at /usr/local/logic/swipl/lib/swipl/library/prolog_stack.pl:487 [12] prolog_debug:assertion_failed(fail,user:false) at /usr/local/logic/swipl/lib/swipl/library/debug.pl:330 [11] prolog_debug:assertion(user:false) at /usr/local/logic/swipl/lib/swipl/library/debug.pl:318 [10] catch(user:assertion(false),_2174,user:format("Caught: ~q~n",...)) at /usr/local/logic/swipl/lib/swipl/boot/init.pl:537 [9] toplevel_call(user:user: ...) at /usr/local/logic/swipl/lib/swipl/boot/toplevel.pl:1113 true.
Even non-interactively:
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 [34] prolog_stack:backtrace(10) at /usr/local/logic/swipl/lib/swipl/library/prolog_stack.pl:487 [33] 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.
Source
- The assertion-handling source is in
lib/swipl/library/debug.pl
- The message printing source is in
lib/swipl/boot/messages.pl
The 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.
My decision: Kick must_be/2 to the curb, and use assertion/1 instead. IMMV.
WISH:
- 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.
Disabling assertions
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 [user]
:
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.
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: 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.