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).

     spec_info {
       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];
     }
     
     MethodSpecification_attribute {
       u2 attribute_name_index;
       u4 attribute_length;
       u4 BML_flags;
       formula_info requires;
       u2 spec_count
       spec_info spec[spec_count];
     }

[This format does not require desugaring into single method spec.] 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. [MH 27022008: added BML_HELPER. Ownership modifiers should be added] 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.
• requires - the binary representation of a formula which is the general precondition of the method, i.e., the disjunction of precondition from all specification branches.
• spec_count - number of specification branches in the specification table
• spec - the specification table, where each element is a spec_info structure. Its fields have the following structure:
  • 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