7.6 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.6.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;
       u2 specs_count;
       {
         u2 access_flags;
         formula_info requires;
         assignable_info assignable;
         formula_info ensures;
         u2 signals_exception_index;
         formula_info signals_formula;
         u2 signals_only_count;
         u2 signals_only_indexes[signals_only_count];
       } specs[specs_count];
     }

The meaning of the fields is as follows:

• attribute_name_index - index in the primary 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. 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.

• specs_count - the number of specification branches
• specs - the table of specification branches, where each element has the following meaning:
• access_flags - the modifier of the specification branch. The only allowed flags are ACC_PUBLIC, ACC_PROTECTED, ACC_PRIVATE. Only one of them can be set.
• requires - the precondition of this specification branch
• assignable - the assignable clauses
• ensures - the normal post-condition of this specification branch
• signals_exception_index - index in the Combined Constant Pool where the exception class name of the exceptional post-condition 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 exceptions enumerated in the signals_only clause
• signals_only_indexes - signals_only clauses: indexes of the exception class names in the Combined Constant Pool - only exceptions of a subclass of one of these classes can be thrown by the method.

7.6.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 primary 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 Combined 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 whose the Code Attribute contains a LocalVariableTable Attribute, 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, or are 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.