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 the 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 the 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 classheader classbody
fileheader ::= packageinfo [imports]
classheader ::= Java class header
classbody ::= [ staticsection ] [ objectsection ] constructors [ methods ]
staticsection ::= [ staticfields ] [ staticspec ]
staticspec ::= [ staticinvariant ] [ staticconstraint ]
[ staticrepresents ] [ staticinitially ]
objectsection ::= [ objectfields ] [ objectspec ]
objectspec ::= [ objectinvariant ] [ objectconstraint ]
[ objectrepresents ] [ objectrepresents ]
constructors ::= constructor [ constructor ]...
imports ::= [ import ]...
staticfields ::= [ staticfield ]...
objectfields ::= [ objectfield ]...
methods ::= [ method ]...
The modifiers follow the order suggested in the JML reference 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.
Each method has the following format:
method ::= [ methodspec ] methodheader [ methodbody ]
Note that the method body may contain both byte code instructions and BML specifications.