Run-Time Checking of Assertions for SWI-Prolog

To install the Run-Time checker of assertions, just follow the next sequence of commands in your SWI-Prolog shell:

  $ swipl
  
  ?- pack_install('https://github.com/edisonm/rtchecks.git').
  true.

Based on the run-time checker of Ciao Prolog.

The semantic of run-time checks is explained in the paper, although is out of date:

http://clip.dia.fi.upm.es/papers/assert-lang-disciplbook_bitmap.pdf

This package provides a complete implementation of run-time checks of predicate assertions. The program is instrumented to check such assertions at run time, or during debugging, and any unsatisfied property is reported.

There are two main applications of run-time checks:

• To improve debugging of certain predicates, specifying some expected behavior that is checked at run-time with the assertions.

• To avoid manual implementation of checks that should be done in some predicates, leaving the code clean and understandable.

The run-time checks can be configured using prolog flags. Below we list the valid prolog flags with its values and a brief explanation of the meaning:

• rtchecks_level

  • exports: Only use rtchecks for external calls of the exported predicates.
  • inner : Use also rtchecks for internal calls. Default.

• rtchecks_status

  Contains a list of the assertion statuses to be checked, could be a list of [true, false, check, debug, static]. Default value is [check, static].

• rtchecks_static

  Contains a list of the assertion statuses to be instrumented statically, could be a list of [true, false, check, debug, static]. Default value is [static].

• rtchecks_entry

  • no : Disable rtchecks for entry assertions.
  • yes : Enable rtchecks for entry assertions. Default.

• rtchecks_exit

  • no : Disable rtchecks for exit assertions.
  • yes : Enable rtchecks for exit assertions. Default.

• rtchecks_abort_on_error

  Controls if run time checks must abort the execution of a program (by raising an exception), or if the execution of the program have to continue.

  Note that this option only affect the default handler and the predicate @pred{call_rtc/1}, so if you use your own handler it will not have effect.

  • yes : Raising a run time error will abort the program.
  • no : Raising a run time error will not stop the execution, but a message will be shown. Default.