7.5 Code Attributes

These attributes represent BML elements which are relevant for the implementation of a method. In particular they are irrelevant for abstract methods.

Most attributes contain tables of BML elements which refer some code instructions (e.g. a BML set instruction is located at a particular point in the method code). Since there may be more than one BML element in a given point of the method code, each BML specification has an order field next to the pc field, specifying what is the relative position of a given BML specification in the sequence of BML specifications occurring at this pc. Order fields of different BML specifications must be different, they do not have to be consecutive numbers. BML specifications with smaller order values are assumed to appear before specifications with greated order values.

The attributes are as follows:

• LocalVariableModifiers - table of BML modifiers of local variables
• LocalGhostVariables attribute - table of local ghost variables
• Assert - table of asserts
• Set - table of ghost set instructions
• LoopSpecification - table of loop specifications
• BlockSpecification - table of block specifications

• The LocalVariableModifiers attribute
• The LocalGhostVariables attribute
• The Assert attribute
• The Set attribute
• The LoopSpecification attribute
• The BlockSpecification attribute