7.1 Encoding of Modifiers

BML modifiers, see Modifiers, are encoded in suitable attributes using binary JVM access_flags and BML_flags fields. The bit values of BML_flags and their summary meaning is given in the following table:

BML_SPEC_PUBLIC = 0x00000001

a Java feature (method/field etc.) declared as public for specification purposes; it can only be used when the feature has a more restrictive visibility in Java; this flag is equal to the 16-bit ACC_PUBLIC JVM flag

BML_SPEC_PROTECTED = 0x00000004

a Java feature (method/field etc.) declared as protected for specification purposes; it can only be used when the feature has a more restrictive visibility in Java; this flag is equal to the 16-bit ACC_PROTECTED JVM flag

BML_NON_NULL = 0x00000020

a feature (field, method result, method's parameter, local variable etc.) which cannot be null

BML_NULLABLE = 0x00000040

a feature (field, method result, method's parameter, local variable etc.) which can be null

BML_PURE = 0x00000080

a method (or class or interface) that does not have side effects

BML_HELPER = 0x00000100

a method which does not have to respect invariants and history constraints

BML_PEER = 0x00000400

ownership modifier for peer features (field, method result, method's parameter, local variable etc.)

BML_REP = 0x00000800

ownership modifier for rep features (field, method result, method's parameter, local variable etc.)

BML_READONLY = 0x00001000

ownership modifier for readonly features (field, method result, method's parameter, local variable etc.)

BML_ELEM_PEER = 0x00002000

ownership modifier for features (field, method result, method's parameter, local variable etc.) with arrays containing peer elements

BML_ELEM_READONLY = 0x00002000

ownership modifier for features (field, method result, method's parameter, local variable etc.) with arrays containing readonly elements

Note that for a given feature (field, method result, method's parameter, local variable etc.) at most one of SPEC_PUBLIC, SPEC_PROTECTED can be set (when applicable), at most one of BML_NON_NULL and BML_NULLABLE (when applicable), at most one of BML_PEER, BML_REP, BML_READONLY (when applicable), and at most one of BML_ELEM_PEER and BML_ELEM_READONLY (when applicable).