| [ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
JML uses specification inheritance to impose the specifications of supertypes on their subtypes [Dhara-Leavens96] [Leavens-Naumann06] [Leavens06b] to support the concept of behavioral subtyping [America87] [Leavens90] [Leavens91] [Leavens-Weihl90] [Leavens-Weihl95] [Liskov-Wing94].
In JML, specification inheritance means that instance methods have to obey the specifications of all methods they override. This, together with the inheritance of invariants and history constraints, forces subtypes to be behavioral subtypes [Dhara-Leavens96] [Leavens-Naumann06] [Leavens06b].
See the report, "Desugaring JML Method Specifications" [Raghavan-Leavens05] for more about the details of specification inheritance in JML.
[[[This needs more work..., examples, etc.]]]
| [ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |