Next: Notations and Conventions Used, Previous: Top, Up: Top
The Bytecode Modeling Language (BML) is a notation for formally specifying the behavior and interfaces of Java bytecode [Lindholm-Yellin] classes and methods. It is closely related to JML, and inherits most of its semantics [Leavens-Baker-Ruby99][Leavens-Baker-Ruby06].
This reference manual records the design and detailed solutions used in BML. It describes the syntax and semantics of the language, referring to appropriate parts of the JML Reference Manual, whenever the BML semantics is inherited from the JML semantics. The second part of the manual describes the kind of tool support that will be provided for BML: a type checker, a verification condition generator and a specification compiler, that can compile JML specifications into BML specifications. A general overview of BML can be found in [BurdyHP07].
This manual is organised as follows. The next two chapters summarise the notations and conventions that we use, and recapitulate the essentials of the bytecode format. Then we present the different aspects of the BML specification language. First we discuss how classes and interfaces can be specified, then we describe the predicate and specification language for BML, and finally we describe how we handle statement annotations. This part concludes with a description how BML specifications are stored in the class file format. The second part of the manual describes the tool support that will be provided for BML.