Inheritance of type definitions - BML Reference Manual

Next: Modifiers for type definitions, Previous: Class and interface definitions, Up: Class and interface definitions

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