Introduction

As I was studying Computer Science I met with the so called Hoare logic. Its main idea is that for each command/program you can define a precondition and a postcondition. These are logical expressions. Precondition must be true before starting your program. It is mainly checking if all inputs are in the correct range and so on. It can be of course also constant true, that means: there’s no specific precondition for this program. Postcondition must be fulfilled after running your program. Like your precondition is x > 0, your program is doing nothing else then y := x, then your post condition will be: x > 0 and x = y. With some predefined rules you can prove with methods of logic that your program is correct or not. It’s pretty easy in case of simple programs, but in case of complex programs it becomes quite complicated, that’s why it is really not typical to validate a program code in this way. It is a static code validation method anyway.

So I learnt it, passed my exam and forgot about that.

Years later I read about the so called SOLID principles and there was one called Liskov substitution principle. I had a flashback from my studies: “Hmm I have already heard it somewhere”. This principle is the following: “ if S is a subtype of T, then objects of type T in a program may be replaced with objects of type S without altering any of the desirable properties of that program”. It is clear, but what does it mean in fact? It means the following:

Preconditions cannot be strengthened in a subtype.

Postconditions cannot be weakened in a subtype.

Invariants of the supertype must be preserved in a subtype

Hmm, it sounds like Hoare logic and it sounds like something useful. At this point I read a bit more about Design by contract and what I learnt there gave me a much better understanding about how I should implement my programs in OOP.

I would like to show you the main concept.

Contracts of a class

We can talk about three different kind of contracts: invariant, precondition and post condition. Invariant is belonging to a class, pre- and post conditions are belonging to a method.

An invariant is nothing else than a restriction on the state of your class. The state of your class is basically the value of your class variables. For example if you have a class for right-angled triangles your class variables can be: the length of a side, the the length of b side and the the length of c side of the triangle. These variables with their current values represent the state of your class. We know the rule: a*a + b*b = c*c in case of a right-angled triangle. That means if our class stands for right-angled triangle all values which are not fulfilling this condition are invalid, they are not representing a right-angled triangle. So this logical expression (a*a + b*b = c*c) can be your class invariant. This should be true in all cases. It will be checked: at the end of your constructor, at starting any of your class methods and at the end of your class methods. Next to that it is a good practise to keep you class variables private and reach them through setter and getter functions, so that your class can never get an invalid state which is not fulfilling the invariant.

The precondition of a method is a condition checked before starting your method. For example if you have a stretch function for your triangle which is having a parameter called factor your precondition can be that this parameter is greater than 0.

The postcondifition of a method. is checked at the end of the function, it is describing what you are expecting from your method. In case of the stretch function in could be something similar: a = old(a) * factor and b = old(b) * factor and c = old(c) * factor, where old means the value at the start of the method. Here it is also important that you need to think about the whole state of your class. So if it has attributes which should not be changed by the method it should be also specified in the post condition. For example if your representation has also a colour attribute than the post condition should be extended with: colour = old(colour).

Until now it is simple: each method has a pre- and a postcondition and the class has an invariant which is checked after construction and at the start and at the end of each function.

Contracts for sub classes

How does it change if your class has a base class?

Your class is holding the invariant of all of its base classes. So in case of one base class the following needs to be always fulfilled: invariant_of_base_class and invariant_of_your_class. So from a child class you can not break the invariant of the base class.

For example if the right-angled triangle class is derived from a triangle class, an invariant for the triangle class can be: a + b >= c (the sum of length of the two shorter side should be at least the length of the longest side). This invariant should be fulfilled also by the right-angled triangles.

Regarding pre- and post condition:

For an overridden function precondition can not be strengthened as the precondition in the base class. So it can be less strength (like instead of (a < 10 and b < 10) just (a < 10)) or the same as in base class.

For an overridden function postcondition can not be weakened as the postcondition in the base class. So it can be the same or more strength.

And this is called Liskov substitution principle, which is part of SOLID principles.

Maybe it is a bit complicated for the first time, but it says nothing else than: your subclass is a special case of your base class, so it should work for all inputs which are working with the base class and it should produce the same results as well.

Support of design by contract in programming languages

Using design by contract for your code is a defensive programming method, your program will have a runtime error in case of the violation of any contract (invariant, precondition or postcondition). That’s also usual that the check for the contracts is only activated in the test versions of your code and deactivate in the release version.

There are some programming languages, like Eiffel which are supporting contracts in a native way, but they are not really popular nowadays. For the today popular OOP languages (C++, C#, Java etc.) you can do your own implementation, it is also not too complicated or reuse an already existing library. For C++ Boost.Contract is a good choice. For Java there are several open-source solutions, like Oval or Contract for Java. For C# you can use Code Contracts. For Python PyContracts.

Summary

Of course I know that design by contract is not an often used way of programming and I think it is totally OK. On the other hand in my view this is a fast and easy way to improve your code quality and make yourself thinking a bit more about “what my code is really doing”. It makes also your code cleaner, because you will double check what should be really the state of your class and your pre- and postconditions are documenting the specification of your function as well.

I think even if you are not developing with this approach it is good to know about this way of programming and think a bit about your invariants, pre- and postconditions at implementing your classes to reach a better code quality.