7.5.5 LoopSpecification Attribute

The LoopSpecification attribute represents the table of loop specifications. Its structure is the following:

     LoopSpecification_attribute {
       u2 attribute_name_index;
       u4 attribute_length;
       u2 loops_count;
       {
         u2 point_pc;
         u2 order;
         assignable_info assignable;
         formula_info invariant;
         formula_info variant;
       } loops[loops_count];
     }

[alx: This corresponds to JMLLoop_specification_attribute from D3.1, some fields are different.]

[jch: Don't we need the start_pc/end_pc here?]

The meaning of particular fields is the following:

• attribute_name_index - index in the constant pool of the attribute name (org.bmlspecs.LoopSpecification)
• attribute_length - length in bytes of the whole structure
• loops_count - the number of loop specifications in the table
• loops - the table of loop specifications; the fields in each specification have the following meaning:
  • point_pc - the point in the method code where the loop starts
  • order - the position of the loop specification in BML declarations at code address point_pc
  • assignable - the assignable clause for the loop
  • invariant - the invariant of the loop
  • variant - the variant (well-foundedness argument) of the loop