Next: , Previous: Class and Interface Specifications, Up: Class and Interface Specifications

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:

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 modifiers1.


[1] However, if more advanced specifcation constructs are added to BML in the future, one might want to allow class modifiers.