[ << ] [ >> ]           [Top] [Contents] [Index] [ ? ]

11. Specification Inheritance

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] [ ? ]

This document was generated by U-leavens-nd\leavens on May, 31 2013 using texi2html