The tools which operate on class files enriched with BML attributes may need to show the BML specifications in a textual form. This section defines a recommended layout for the specifications in this format. This does not only concern the layout of BML expressions, but also the way the specifications are embedded in a textual representation of normal class files.
We assume that the spaces in the grammar below denote any sequence of whitespace, where whitespace is defined to be either a usual whitespace character or comment.
As in Java, we allow two kinds of comments, with the same syntax as in Java. Each BML annotation is embedded in a specially formatted comment, starting with /*@ or //@ and terminated by @*/ or the end of line, respectively. We also permit comments which are started with /*@ to be terminated by */. To allow a nice presentation of specifications, inside a BML specification, each line can start with @, possibly preceded with whitespace.
The suggested format of the textual representation of a class file with BML annotations is defined via the following grammar.
classfile ::= fileheader typeheader typebody
fileheader ::= packageinfo constant-pools
packageinfo ::= package packagename nl [ nl ]...
packagename ::= [default] | typename
constant-pools ::= constant-pool [ second-constant-pool ] nl
constant-pool ::= Constant pool: nl constant-pool-content
second-constant-pool ::= Second constant pool: nl constant-pool-content
constant-pool-content ::= constant-pool-line nl [ constant-pool-line nl ]...
constant-pool-line ::= const cp-ref = constant-pool-entry [ constant-pool-comment ]
constant-pool-entry ::= class-cp-entry | field-cp-entry
| method-cp-entry | interface-method-cp-entry
| string-cp-entry | integer-cp-entry | float-cp-entry
| long-cp-entry | double-cp-entry
| name-and-type-cp-entry | utf8-cp-entry
class-cp-entry ::= Class cp-ref;
field-cp-entry ::= Fieldref cp-ref.cp-ref;
method-cp-entry ::= Methodref cp-ref.cp-ref;
interface-method-cp-entry ::= InterfaceMethodref cp-ref.cp-ref;
string-cp-entry ::= String cp-ref;
integer-cp-entry ::= Integer [ sign ] decimal-integer-literal;
float-cp-entry ::= Float [ sign ] floating-point-literal;
long-cp-entry ::= Long [ sign ] decimal-integer-literal;
double-cp-entry ::= Double [ sign ] floating-point-literal;
name-and-type-cp-entry ::= NameAndType cp-ref.cp-ref;
utf8-cp-entry ::= Utf8 [ string-character ]...;
cp-ref ::= #decimal-numeral
constant-pool-comment ::= // [ non-end-of-line ]...
typename ::= ident[/typename]
typeheader ::= classmodifiers class ident
[ class-extends-clause ] [ implements-clause ] nl...
| interfacemodifiers interface ident
[ interface-extends-clause ] [ implements-clause ] nl...
classmodifiers ::= [ classmodifier ]...
interfacemodifiers ::= [ interfacemodifier ]...
classmodifier ::= public | protected | private
| abstract | static
| final | strictfp
interfacemodifier ::= public | protected | private
| abstract | static |
| strictfp
class-extends-clause ::= extends typename
interface-extends-clause ::= extends name-list
implements-clause ::= implements name-list
name-list ::= typename [, typename ]...
typebody ::= [ staticsection ] [ objectsection ] [ methods ]
staticsection ::= [ staticfields ] [ staticspec ]
staticspec ::= [ staticinvariants ] [ staticconstraints ]
[ staticrepresents ] [ staticinitially ]
objectsection ::= [ objectfields ] [ objectspec ]
objectspec ::= [ objectinvariants ] [ objectconstraints ]
[ objectrepresents ] [ objectinitially ]
staticfields ::= [ staticfield ]...
objectfields ::= [ objectfield ]...
staticinvariants ::= [ static invariant nl ]...
staticconstraints ::= [ static history-constraint nl ]...
staticrepresents ::= [ static represents-decl nl ]...
staticinitially ::= [ static initially-clause nl ]...
objectinvariants ::= [ invariant nl ]...
objectconstraints ::= [ history-constraint nl ]...
objectrepresents ::= [ represents-decl nl ]...
objectinitially ::= [ initially-clause nl ]...
methods ::= [ method ]...
staticfield ::= static field
objectfield ::= field
The non-terminals ident, sign, decimal-integer-literal, floating-point-literal, string-character, decimal-numeral, and non-end-of-line are defined as in the JML reference manual. We assume that certain tokens are terminated with a newline character. This is marked with the use of the nl terminal. Additionally, the modifiers follow the order suggested in the JML manual. Note that the format admits only one definition of a class in a textual file. This is due to the fact that each class file contains only one class definition. This is also the reason why we omit the braces ({ and }) around the class body. We additionally assume that classheader is included in a single line.
[AS 29092008: invariants and the-likes with no desugaring ]
The format of method, field, and clinit declarations is given in the section Class Member Declarations.
Internally, variable names are represented as references into the constant pool or the local variable table. However, tools can display the original variable names, to improve readability of the specifications.