The Firing of Assertions

When the condition of an assertion statement evaluates to false, the assertion is fired. When an assertion is fired, the user is supplied with some useful debugging information. This information can be used to determine exactly which assertion statement fired, and can aid in determining why that statement fired. Each of the assertion types listed above produce a similar output when they are fired. In C++ this output looks like:

<process ID>: <assertion type> <condition> failed at <file name>:<line number>

The <process ID> is the unix process ID of the executable program that contained the assertion that fired. The <assertion type> tells whether the assertion that fired was a pre-condition, post-condition, assertion, or invariant. The <condition> is the condition that failed, causing the assertion to fire. The <file name> is the name of the file that contains the source code of the location where the assertion fired, and the <line number> is the line in this file where the assertion was fired.

The <file name> and <line number> outputs of Specification Placed assertions are adjusted to reflect the location in the source code that they were evaluated at. This means that a PRE_CONDITION statement that is Specification Placed will show the file name and line number that identifies the opening ``curly brace'' of that method's definition. This feature is even more useful when dealing with POST_CONDITION and INVARIANT statements. When a POST_CONDITION fires in a method that has multiple exit points, the file name and line number can be used to determine which exit point was being executed when the assertion fired. Similarly, the firing of an INVARIANT can be traced to discover exactly where execution was when it failed.

The following is an example of a POST_CONDITION firing during the running of an executable. The file ``cls.cxx'' is a library file that is being used by the compiled program ``test_double''.

cls.cxx:

. . . .

37: /* DoubleInt(int x)
38:  *    This function takes an integer as its parameter, and returns an 
39:  *    integer that is twice as large as the integer that it was given.
40:  */
41: int
42: DoubleInt (int x)
43: {
44:   POST_CONDITION ($RETURN == ($OLD(x) * 2), "Failed to double the variable");
45: 
46:   x *= 3 ;     // This is where the error occurs!
47:   return x ;
48: }

. . . .

When the program is run...

rst_computer> test_double
process 11350: post-condition ( $RETURN == ( $OLD ( x ) * 2 )  ) 
failed at cls.cxx:47
[Failed to double the variable]

Notice that the file name indicated (``cls.cxx'') is the the name of the library file that contains the DoubleInt function, not the name of the program that was executed. Also notice that the line number that is displayed is the line number of the return statement (47), not the line number of the post-condition. This information makes it simple to track down the bug in this program.

In Java, the message that is displayed is slightly different due to the different capabilities of the language. In Java, no process id is displayed. Java does give the added information of an entire stack trace where the line number and file name are displayed in C++. An example of an assertion firing in Java would look something like:

rst_computer> java prime
PostCondition ($ForAll ( int , x , 0 , 5 , q [ x ] > - 1 ) ) failed:
        at prime.arr_test(prime.java:77)
        at prime.main(prime.java:116)
[negative int existed]