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
             | helper | non_null | nullable
             | 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 thus the 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 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.