7.4 Method Attributes

BML-related method attributes are added as additional attributes to regular methods in the Method table (see Methods Data Structure). The attributes are as follows:

• MethodSpecification - pre and post-conditions and other specification clauses of the method
• ParameterTable - information on the method parameters (e.g., BML modifiers, names etc)

7.4.1 MethodSpecification Attribute

This attribute contains the specification of a single method, without references to its implementation (as specified in the Code Attribute).

     MethodSpecification_attribute {
       u2 attribute_name_index;
       u4 attribute_length;
       u4 BML_flags;
       formula_info spec_requires;
       u2 assignable_count;
       assignable_info assignable[assignable_count];
       formula_info ensures_formula;
       u2 signals_count;
       {
         u2 exception_index;
         formula_info signals_formula;
       } signals[signals_count];
       u2 signals_only_count;
       u2 signals_only_indexes[signals_only_count];
     }

The meaning of the fields is as follows:

• attribute_name_index - index in the constant pool of the attribute name (org.bmlspecs.MethodSpecification)
• attribute_length - length in bytes of the whole structure
• BML_flags - the flags that are set for the method. The allowed flags are BML_PURE, BML_NON_NULL, BML_NULLABLE, BML_SPEC_PUBLIC, BML_SPEC_PROTECTED, BML_HELPER, BML_PEER, BML_REP, BML_READONLY, BML_ELEM_PEER, BML_ELEM_READONLY. [MH 27022008: added BML_HELPER. Ownership modifiers should be added - DONE (jch)] All other flags must be cleared. Only one of BML_NON_NULL, BML_NULLABLE can be set. Only one of BML_SPEC_PUBLIC, BML_SPEC_PROTECTED can be set. Only one of BML_PEER, BML_REP, BML_READONLY can be set. Only one of BML_ELEM_PEER, BML_ELEM_READONLY can be set only if one of BML_PEER, BML_REP, BML_READONLY is set and the method's result is an array.

  The BML_NON_NULL/BML_NULLABLE modifiers as well as ownership modifiers concern the result value of the method.

• spec_requires - the precondition of this specification branch
• assignable_count - number of assignable clauses
• assignable - the assignable clauses
• ensures_formula - the normal post-condition of this specification branch
• signals_count - number of exceptional post-conditions
• signals - table of exceptional post-conditions; each element has the following fields:
  • exception_index - index in the constant pool where the exception class name is stored
  • formula_info signals_formula - the exceptional post-condition to be met when the exception referenced above is thrown
• signals_only_count - number of signals_only exceptions
• signals_only_indexes - signals_only clauses: indexes of the exception class names

7.4.2 ParameterTable Attribute

The ParameterTable attribute represents the BML related information about the method parameters. The structure of the attribute is as follows:

     ParameterTable_attribute {
       u2 attribute_name_index;
       u4 attribute_length;
       u2 parameters_count;
       {
         u2 name_index;
         u2 access_flags;
         u4 BML_flags;
         u2 index;
       } parameters[parameters_count];
     }

The meaning of the fields is as follows:

• attribute_name_index - index in the constant pool of the attribute name (org.bmlspecs.ParameterTable)
• attribute_length - length in bytes of the whole structure
• parameters_count - the number of parameters of the method. It must be equal to the number of parameters in the method's type description.
• parameters - the table of parameter descriptions, where each element is a structure containing one field:
  • name_index - the index in the first or the second constant pool where the parameter's name is stored as a CONSTANT_Utf8_info element
  • access_flags - the JVM flags that are set for the given parameter. The only allowed flag is ACC_FINAL. All other flags must be cleared.
  • BML_flags - the BML flags that are set for the given parameter. The allowed flags are BML_NON_NULL, BML_NULLABLE, BML_PEER, BML_REP, BML_READONLY, BML_ELEM_PEER, BML_ELEM_READONLY. All other flags must be cleared. Only one of BML_NON_NULL, BML_NULLABLE can be set. Only one of BML_PEER, BML_REP, BML_READONLY can be set. Only one of BML_ELEM_PEER, BML_ELEM_READONLY can be set only if one of BML_PEER, BML_REP, BML_READONLY is set and the parameter is an array.
  • index - the index by which the parameter is referenced in the BML expressions and the code of this method

Note that for methods where the Code attribute (see Methods Data Structure) contains a LocalVariableTable attribute (see again Methods Data Structure) the parameter names can already be stored in this table. In this case the two names must be equal. However, for methods without the Code attribute (because they are declared in an interface, abstract or native) the parameter's name is only stored in this attribute.

The index field in each parameter description must correspond to the index by which this parameter is referenced in the code (if it is present) and BML expressions in the method specification and other formulas in the method's code. Note that if there are long integer or double float parameters in the list, the value of the index does not have to be equal to the position of the parameter in the method's signature.

The order of parameters is not specified and not all of them must be described in the table, but any parameter must be described at most once.