Did you know ... Search Documentation:
Predicate assertion/1
Availability::- use_module(library(debug)).(can be autoloaded)
Source[det]assertion(:Goal)
Acts similar to C assert() macro. It has no effect if Goal succeeds. If Goal fails or throws an exception, the following steps are taken:

  • call prolog:assertion_failed/2. If prolog:assertion_failed/2 fails, then:

    • If this is an interactive toplevel thread, print a message, the stack-trace, and finally trap the debugger.
    • Otherwise, throw error(assertion_error(Reason, G),_) where Reason is one of fail or the exception raised.
Tag confusing pages with doc-needs-help|Tags are associated to your profile if you are logged in|Report abuse
Tags:
  • doc-needs-help
  • exceptions
LogicalCaptain said (2016-12-15T17:36:01):0 upvotes 0 0 downvotes
Picture of user LogicalCaptain.

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