Design by contract and class invariant

Question

hi

I'm reading about dbc (http://en.wikipedia.org/wiki/Design%5Fby%5Fcontract) Can someone please give me a simple example of using class invariants in relation to inheritance?

Answer 1

Design by contract concepts get slightly complicated when they are adapted to object-oriented languages.

A class invariant is a property that each instance of the class is guaranteed to have when a method is called (like a common pre-condition for all methods), and that in return each method and constructor must ensure remains true when they terminate (like a common post-condition).

They are good for expressing consistency conditions. A Wallet class that modelizes an actual wallet might have the class invariant that the amount contained is always positive.

Class invariants, like the rest of the contract, are inherited. New implementations of methods must provide the same guarantees as the methods they replace.

Answer 2

In the inherited class, the invariants should be at least equally strict, but they can be stricter. If an invariant is omitted in a derived class, the invariants of the base class apply of course.

eg :

// Class invariant : sum should be > -1000
Account { public int sum; }

// Class invariant : sum should be >= 0
AccountForKids : inheritsFrom Account { public int sum; }

The account for kids shouldn't go beneath zero, but that of course is bigger than -1000.

In General : The contract of a derived class is always hounoured when the class invariants become stricter.

Answer 3

A derived class invariant should:

• Check the invariants of any member variables introduced in the dervied class
• Check the invariant of the base class