4. Extensions

Extensions

An extension is pure if doesn’t modify the specification of inherited methods. Therefore it can only extend the base specification adding new operations and is able to alter the implementation of the inherited methods following the specification. A subclass has the same AF of its parent, whilst it inherits RI without modifications adding a new RI.

In a non-pure extension the specification is altered in one or more inherited methods. This kind of extension should be avoided.

Liskov Substitution Principle (LSP)

Liskov substitution principle:

subtypes must be behaviorally substitutable for their base types.

In JML we must assure that:

• no new exceptions should be thrown in derived class
• pre-conditions cannot be strengthened
• post-conditions cannot be weakened
• invariants must be preserved

To ensure LSP in an extension one needs to do a logic OR (||) of the pre-conditions and a logic AND (&&) of the post-conditions.

tl;dr

require no more, promise no less.