7.4.1 MethodSpecification Attribute

This attribute contains the specification of a single method not referring to its components (e.g. line numbers).

     spec_info {
       formula_info spec_requires;
       u2 assignable_count;
       assignable_info assignable[assignable_count];
       formula_info ensures_formula;
       u2 exsures_count;
       {
         u2 exception_index;
         formula_info exsures_formula;
       } exsures[exsures_count];
     }
     
     MethodSpecification_attribute {
       u2 attribute_name_index;
       u4 attribute_length;
       u2 BML_flags;
       formula_info requires;
       u2 spec_count
       spec_info spec[spec_count];
     }

[alx: this corresponds to JMLMethod_attribute, significant differences with D3.1]

The meaning of the fields is the following:

• 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. JCh: anything else? All other flags should be cleared.
• requires - the binary representation of a formula which is 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
  • exsures_count - number of exceptional post-conditions
  • exsures - table of exceptional post-conditions; each element has the following fields:
    • exception_index - index in the constant pool where the exception class is stored
    • formula_info exsures_formula - the exceptional post-condition to be met when the condition referenced above is thrown