The Assertion Language

The assertion language that RST developed is used to specify the condition that an assertion statement is verifying. It functions as an extension of the syntax that C++ and Java provide. The assertion language provides a means to simplify the creation of complex boolean expressions. An assertion is fired when one of these boolean expressions evaluates to false. RST's assertion language extends the power of boolean expressions and make them more readable. The following language constructs are provided (and can be joined with any standard C++ / Java expression):

$NOT, $AND, $OR

These are just textual equivalents of ``!'', ``&&'', and ``'' respectively. They help to increase code readability.

$Always

Evaluates to false; used to cause an assertion to fire unconditionally. Analogous to ( false ).

$Zero(<variable>)

Evaluates to false if <variable> is not zero. Analogous to (<variable> == 0).

$Equal(<var1>, <var2>)

Evaluates to false if <var1> does not equal <var2>. Analogous to (<var1> == <var2>).

$Range(<variable>, <lower>, <upper>)

Evaluates to false if <variable> is not between <lower> and <upper>. Analogous to ((<variable> >= lower) && (<variable> < upper))

$StringCompare(<string1>, <string2>)

The string parameters must both be type char *. Evaluates to false if the strings are not identical.

$ForAll(<type>, <iterator>, <initialization>, <stop>, <condition>)

The $ForAll statement is can be used to ensure that every element of an array or STL container meets some condition. It is based on the mathematical concept of universal quantification. The user must supply the iterator and its type. He must also provide the initialization value for the iterator, and the stopping criteria. The <condition> is checked at each iteration of the loop. The <condition> may be a simple expression, or it may be a complex expression built using any of the elements of the assertion language. This includes the ability to nest $ForAll statements within other $ForAll or $ThereExists (see below) statements. The following is an example of using a $ForAll statement in an assertion statement.

. . . .
int grades[10] ;
. . . .
ReadGrades(grades) ;
ASSERT($ForAll (int, i, 0, 10, grades[i] >= 0), 
       "No negative grades allowed") ;
. . . .

This assertion statement will fire if any of the integers stored in the array grades (between 0 and 9 inclusive) are negative.

$ThereExists(<type>, <iterator>, <initialization>, <stop>, <condition>)

The $ThereExists statement follows the same format as the $ForAll statement. It is based on the mathematical concept of existential quantification. It will fire only if the condition fails for every iteration of the loop. Like the $ForAll statement, it too may be nested or combined with any element of the assertion language. The expression:

  ThereExists(int, i, 0, 10, grades[i] >= 65)

will evaluate to false only if none of the integers stored in grades (between 0 and 9 inclusive) are greater than 65.

$RETURN and $OLD(<variable>)

These two keywords are available for use only in a POST_CONDITIOIN statement. The $RETURN keyword refers to the value being returned by the function at whatever return statement has been reached.
The $OLD(<variable>) keyword is used to reference the value of the variable <variable> at the entrance to the method / function.
The $OLD and $RETURN keywords can be combined and used as follows:

int
DoubleInt (int x)
{
  POST_CONDITION($RETURN == $OLD(x) * 2), "Failed to double the variable") ;
  x *= 2 ;
  return x ;
}

In this example, the POST_CONDITION is ensuring that the value that is returned by DoubleInt() is twice that of what was passed in.