4.1 Class and Interface Definitions

Classes and interfaces allow to define new types for Java (bytecode). They are quite similar: interfaces can be considered as a special class definition, with as main difference that method attributes do not contain the Code Attribute. In BML there is one exception to this: interfaces can contain model methods with implementation. Each type definition is stored in a separate class file, whose format is described in The Class File Format.

4.1.1 Inheritance of Type Definitions

Inheritance in BML is defined similarly as inheritance for Java or JML, see Section 6.1.1 of the JML Reference Manual. As in JML, ghost and model features as well as specifications are inherited, i.e., a subtype inherits from its supertypes:

• all instance fields, including model and ghost fields
• instance methods (including model methods), together with their specifications
• instance invariants and instance history constraints

As in JML, instance methods have to obey the specifications of all methods that they override. Together with inheritance of invariants and history constraints, this enforces behavioural subtyping [Dhara-Leavens96] [Leavens-Naumann06] [Leavens06b].

4.1.2 Modifiers for Type Definitions

BML does not have any BML class modifiers¹.