Figure 17: BSL assertion syntax
Figure 17 gives the syntax of BSL assertions.
Sets of assertions are defined using the Javadoc tag @assert in
the header documentation for methods or constructors. Each assertion
set defined by an @assert tag can be given an optional name,
and this name along with the name for each assertion in the set, is
used to uniquely identify the assertion so that it be can be
selectively enabled/disabled. If the set name is omitted, the fully
qualified name of the corresponding method is used as the name for the
assertion set. The optional name is followed by zero or more Java
newline comments.
Besides precondition assertions as illustrated above, BSL supports
location assertions and postcondition assertions.
LOCATION[<label>] <assertion-name>: <exp>
is satisfied if <exp> is true when control is at the Java
statement labeled by <label> in the corresponding method).
POST <assertion-name>: <exp> is satisfied
if <exp> is true immediately after the execution
of any of the corresponding method's return statements
or after the execution of the last statement in the method
if it has no return statement. The expression <exp>
can refer to the return value of the method using the
Bandera reserved identifier $ret.
There are various other well-formedness conditions associated with variable scoping that we will not discuss in detail here. For example, a precondition assertion cannot reference local variables for the method since these have not been initialized when the byte-code for the method body begins executing, and a label assertion can only reference variables are in scope at the point where the given label appears in the source code.
Once assertions have declared, a selection of the assertions can be presented to Bandera as an assertion specification to be model-checked. Figure 15 presents a BSL file where the first specification BufferAssertions enables checking of the PositiveBound as declared in Section 5.6. Violated assertions are reported back to the user by presenting a trace through the source program that terminates at the location in which the data condition is violated.