4.2 Modifiers

The following is the syntax of Java modifiers.

     modifiers ::= [ modifier ] ...
     modifier ::= public | protected | private
             | abstract | static |
             | final | synchronized
             | transient | volatile
             | native | strictfp
             | const

All these modifiers are kept as access flags in the appropriate class file attributes.

BML inherits the following modifiers from JML.

     bml-modifier ::= spec_public | spec_protected
             | model | ghost | pure
             | static | helper
             | non_null | nullable
             | ownership-modifier
     ownership-modifier ::= peer | rep | readonly

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 therefore the static modifier is obligatory, and therefore one does not need the instance modifier in the grammr. The modifiers are added as special BML flags to the appropriate attributes in the class file (see Encoding of BML in Class File Format). There are no BML flags for the modifiers ghost and model. 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.