6.1 Annotation Statements

In contrast to JML, annotation statements in BML are not directly inserted in the code. Instead, they are stored in a separate list, with a special index that denotes the program counter of the instruction that the annotation is attached to. The annotation statement is supposed to be evaluated before the instruction is evaluated. It can happen that several annotations are associated with the same statement, and that the evaluation order is important, for example in the following (source) code fragment.

     // set x = y + z;
     // assert x != 0;
     // set w = r/x;
     t = compute(y, z, r);
     // assert t > x + w;

To properly encode such a specification, the attributes that describe the annotation statements in BML contain a special order field, that specify in which order the annotations should be evaluated, see Code Attributes.

BML supports the following annotation statements: assert, assume, set, unreachable and debug. Their semantics corresponds to their JML semantics, as described in Chapter 12 of the JML Reference Manual. (As an aside: in static verification, an assume statement is considered to add extra information to whatever is known to hold for this program point; it does not replace this information, and thus does not have to be strong enough by itself to complete the verification of the method.)

Since Java 1.5, source code can contain explicit assert statements. In JML these are treated in the same way as JML assert annotations, i.e., both runtime and static checking consider the assert predicates. In bytecode, the explicit assert statements are encoded using a conditional instruction. A special AssertError is thrown if the assertion is violated during execution. If at BML level, one wishes that the assert statements are also considered as part of the specification, one needs to add them explicitly to the list of assert attributes. Typically, a JML to BML compiler will have a special flag to take care of this.