4.3 Java Member Declarations

Member declarations are method, field or class initializer declarations. Method and field declarations can be annotated with BML-modifiers. The presence of these modifiers is signalled by setting appropriate access flags in the BML-access flags attributes in the extended class file.

[Question for WU: will there be special BML-access flags attributes?]

The BML-modifiers that can used for method declarations are spec_public, spec_protected, model, pure, non_null and helper. In addition, each of the method's parameters can be annotated with a modifier non_null or nullable.

[non_null and nullable can be modifiers on parameters. WU will make a proposal how to encode them in bytecode format.]

The BML-modifiers that can be used for field declarations are spec_public, spec_protected, model, ghost, non_null, nullable and instance.

The semantics of the method and field modifiers is described in Section 6.2 and Section 7.1.1 of the JML Reference Manual.

Fields can be specified to belong to a data group. The class file contains a special attribute list with all data groups declared in the program. BML only supports static inclusion in data groups. This means that each element in the data group list contains a list of fields that are part of the data group. For more information about data groups and their semantics, see Chapter 10 of the JML Reference Manual.

[Question for WU: is this a reasonable implementation?]

At source level, each field declaration contains a name and a type specification. JML allows one to use a special type \TYPE for ghost or model variables (see Section 7.1.2.2 of the JML Reference Manual). This type represents the kind of all Java types. At bytecode level, the type information is encoded as a string in the attribute descriptor entry in the constant pool. The descriptor entry for the \TYPE type is stored in the second constant pool.

[Question to WU: do you agree?]

The special type annotations peer, rep and readonly are stored as special access flags of the field attribute. For more information about the universe type system that is encoded with these attributes, see Chapter 18 of the JML Reference Manual.

[Conclusion about class initialisers: see static; in ../examples/static-ghost-variables/SimpleYear.bytecode] TO BE DISCUSSED MORE

[INRIA: I'm not so sure anymore about the discussion that we took, i.e. to leave the initalisation of the static ghost variable in JML syntax. All BML annotations need to be stored in the class file, so we would need to define a good format for doing this. Maybe the second proposal, adding ghost code for the initalisation of the ghost field is much simpler. CONCLUSION: WU will come with a proposal to store this as a special attribute.]