Promela Reference -- assert(4)





assertion statement - for stating simple safety properties.

assert( expr )



An assert statement is similar to the predefined condition statement skip in the sense that it is always executable and has no other effect on the state of the system than to change the control-state of the process that executes it. A very desirable side-effect of the execution of this statement is, however, that it can trap violations of simple safety properties during verification and simulation runs with Spin.

The assert statement takes an expression as its argument. The expression is evaluated each time the statement is executed. If the expression evaluates to the boolean value false (or, equivalently, to the integer value zero), a violation of the correctness requirement is reported, but the system execution is not necessarily interrupted.


assert(a > b)


The second type of assert statement above is useful to mark a local state in a proctype that is required, or assumed, to be unreachable. If the statement is reached nonetheless, it will be reported as an assertion violation.

The assert statement can be used to formalize general system invariants, i.e., boolean conditions that are required to be invariantly true in all reachable system states. To express this, it suffices to place the system invariant in an independently executed process, as in:

active proctype monitor() { assert(invariant) }

where the name of the proctype is immaterial. Since the process instance is executed independently from the rest of the system, the assertion may be evaluated at any time: immediately after process instantiation in the initial system state, or at any time later.

A simulation, instead of a verification, will not necessarily prove that a safety property expressed with an assert statement is valid, because it will check its validity on just a randomly chosen execution. Note that placing a system invariant assertion inside a loop, as in

active proctype wrong() { do :: assert(invariant od }

would still not guarantee that a simulation would check the assertion at every step, because the fact that a statement could be executed at every step does not guarantee that it will be executed in that way. One way to accomplish such a tight connection between program steps and assertion checks would be to use a temporal claim instead of an asynchronous process:
never { do :: assert(invariant) od }

Alas, this would not work for simulation either, because temporal claims are not considered by Spin during random simulations. Simulations are for debugging, not for verification.

skip(1), ltl(1), never(2).

Spin Online References
Promela Manual Index
Promela Grammar
Spin HomePage
(Page Updated: 16 December 1997)