4.3 Class 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.

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

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

In JML, every type can be annotated with an ownership modifier: peer, rep and readonly. For more information about the universe type system that is encoded with these attributes, see Chapter 18 of the JML Reference Manual). At bytecode level, special care has to be taken how this is modelled. First of all, if an array is declared, it can have two ownership modifiers: one for the array structure, and one for the elements in the array (which should not be rep, see [Dietl-Mueller05]). In the textual representation of BML, an array declaration can be modified with two modifiers: the first denotes the modifier for the array structure, the second the modifier for the elements. In the binary BML representation (see Encoding of BML in Class File Format), besides the flags that represent the modifiers peer, rep and readonly, special flags elem_peer and elem_readonly can be set to denote the modifier for the elements in an array. (however, the array ownership flag can not be set without one of the standard ownership flags being set). Another complication is that both specification and code can contain type specifications, (e.g., an expression instanceof T, which can be decorated with ownership modifiers. To handle the occurrence of type specifications in expressions, the binary representation of expressions (i.e., type expression info put ref! ) allows ownership modifiers to occur at appropriate places. To handle the occurrence of type specifications in instructions, the code attributes contain a special put ref Ownership Attribute.

The semantics of the different modifiers is described in Section 6.2, Section 7.1.1, and Chapter 18 of the JML Reference Manual.

Every field declaration implicitly declares a data group. All fields (including ghost and model fields) can be specified to belong to a data group defined by another field. The class file contains a special DataGroups Attribute (see Class Attributes), containing all non-trivial data groups, i.e., data groups that do not contain only the field declaration that defined the data group, but also other fields. 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.

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.

The initialization of ghost fields should be specified by set instructions placed at the beginning of the appropriate initializers: static initializer <clinit> for static fields, and constructors for instance fields. Initialization of local ghost variables should be specified by set instructions inside the method, at the beginning of the variable's scope.