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 more the practical aspects of BML: how specifications can be stored in class files, type checking, compilation from JML to BML, and verification of 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. Then we describe how BML specifications are stored in the class file format, and define type checking of BML specifications. Next, we define the translation from JML to BML specifications, and we discuss verification of BML specifications.