[Next] [Up] [Previous] [Contents]

The assert declaration

A declaration of the form

        assert p;

where p is a temporal formula, means that every execution of the program must satisfy the formula p. An execution that does not satisfy the formula is called a failure of the program.

An assertion may be given a name. For example:

        foo : assert p;

This does not change the semantics of the program, but provides an identifier ``foo'' for refering to the given assertion. The code

        foo : assert p;
        foo : assert q;

is equivalent to

        foo : assert p & q;