The following is the syntax of Java modifiers.
modifiers ::= [ modifier ] ... modifier ::=
All these modifiers are kept as access flags in the appropriate class file attributes.
BML inherits the following modifiers from JML.
Their semantics is the same as for JML, as described in
Section 6.2 of the JML Reference Manual. Unlike in Java and JML, field
declarations in interfaces are not
static by default, and
static modifier is obligatory, and one
does not need the
instance modifier in the grammar.
The modifiers are added as
special BML flags to the appropriate attributes in the class file (see
Encoding of Modifiers).
There are no BML flags for the modifiers
Instead, we declare special class attributes containing a class's ghost
fields, model fields etc.
The suggested order of modifiers in the textual representation of BML annotated bytecode follows that of JML (see Section 6.2.1 of the JML Reference Manual). For the binary representation of BML, the modifiers are not ordered.