7.2.7 Constraint Attribute

This attribute describes the history constraint of the class. It has the following structure:

     Constraint_attribute {
       u2 attribute_name_index;
       u4 attribute_length;
       formula_info constraint;
     }

[alx: this seems to correspond to JMLHistoryConstraints_attribute from D3.1, but the format is different]

The meaning of the fields is the following:

• attribute_name_index - index in the constant pool of the attribute name (org.bmlspecs.Constraint)
• attribute_length - length in bytes of the whole structure
• invariant - the binary representation of the constraint formula.