7 Encoding of BML in Class File Format

The encoding of BML specifications in class files is done via attributes. Appropriately to the kind of encoded specification constructs, class attributes, field attributes, method attributes and code attributes are used. Typically one attribute holds a table of all specifications of one kind, e.g. all class invariants are grouped in a single class attribute (see Invariants Attribute), all set instructions in the body of a given method are grouped in one code-level attribute of that method (see SetTable Attribute).

The structure of every attribute follows the general schema described in Notations for Class File Attributes. The precise description of the format of each attribute is given in subsequent sections. In general, the each item of an atribute structure is either:

• a number, whose size in bytes is denoted by its type: u1, u2, and u4 (see Notations for Class File Attributes),
• a variable-length item array, denoted by the C-like array notation type name[length],
• a variable length encoding of an expression of type expression_info, formula_info or assignable_info (see Encoding of Expressions)

Some of the numbers of type u2 represent indexes in the primary constant pool (like attribute names) or the Combined Constant Pool (see Combined Constant Pool) referencing constants, types, fields, etc.

• Encoding of Expressions
• Combined Constant Pool
• Encoding of Modifiers
• Class Attributes
• Field Attributes
• Method Attributes
• Code Attributes