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:
semantics corresponds to their JML semantics, as described in
Chapter 12 of the JML Reference Manual. (As an aside: in static verification,
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.