1.2 Relation with JML

As said, BML is designed to be very closely related with JML. It inherits all features of JML that are well-understood and that are judged important to specify appropriate security and behavioural properties for mobile code. For these features, whenever possible we define their semantics to be equal to the semantics at source code level. Where necessary, we describe the changes that are due to the adaptation to bytecode level. Further, we refer to appropriate parts of the JML Reference Manual whenever necessary. We assume that the reader has basic knowledge of JML and its basic specification constructs.

Section 2.9 of the JML Reference Manual describes a division of JML into different language levels. Level 0 describes the JML language constructs that should be supported by any JML tool. BML as we define it in this reference manual contains corresponding constructs for all JML language constructs that are in JML level 0, except for the informal description and the debug expression. An informal description can be considered as a comment, and for verification it is replaced by an appropriate default value, as if there was no specification. As comments are not kept at bytecode level, we also consider that there is no need to preserve the informal description at bytecode level. The JML debug expression can contain arbitrary pieces of short code. BML only contains a simplified debug annotation, allowing to express the value of particular variables.

Experience with static formal verification of bytecode applications (which was the motivation for developing BML) has shown that several other JML language constructs are essential for usability and expressiveness as well. Therefore, these language constructs are also part of the BML standard. Typically, these constructs are in JML level 1, the language constructs that should be supported by most JML tools. In particular, it is allowed to use (pure) method calls in specifications.

We would like to point out that there is a difference between adding a BML specifications to a class file, and augmenting a class file for runtime checking of a JML (or BML, for that matter) specification. The BML specifications are stored as special attributes in the class file and can be inspected and manipulated by different tools. When a class file is augmented for runtime checking (i.e., it is compiled with jmlc), appropriate checks are inserted in the bytecode, that will throw an exception whenever it finds that an annotation is violated.

One difference with JML that is inherent to the difference between bytecode and source code is the treatment of the assert instruction in Java 1.5. This instruction is part of the source code language, but compiled into a conditional, traditional bytecode instruction. JML treats Java asserts in the same way as JML asserts, but when compiling the source code, the Java assert is transformed into standard bytecode, and is no longer part of the specification. To solve this problem, the JML to BML compiler has a special option to compile the assert instruction into a BML assert annotation.