Next: , Previous: Annotation (of) Statements, Up: Top


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:

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.