Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Design by contract and class invariant

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

like image 660
loudiyimo Avatar asked Feb 27 '23 23:02

loudiyimo


2 Answers

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.

like image 83
Pascal Cuoq Avatar answered Mar 05 '23 14:03

Pascal Cuoq


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.

like image 34
Peter Avatar answered Mar 05 '23 14:03

Peter