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:
u4(see Notations for Class File Attributes),
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.