Design by Contract in Practice

Design by Contract (DbC) is a very valuable specification technique -- I already posted about it in German (Netze spannen mit Design by Contract). However, you should be aware that DbC also tends to complicate matters if state is involved. In this case, we need a complementing approach.

To give you a simple example, have a look at a thing called "Account". The "Account" is purely specified via pre- and post-conditions (require and ensure); "context" enables you to capture a context required for a subsequent post-condition. The code is written in a syntax close to Python. A contract precedes the method signature.

class Account(object):
    ensure: self.balance == 0
    def __init__(self)

    require: 0 < amount <= self.balance
    context: balance = self.balance
    ensure: self.balance == balance - amount
    def withdraw(self,amount)

    require: amount > 0
    context: balance = self.balance
    ensure: self.balance == balance + amount
    def deposit(self,amount)
        
    context: balance = self.balance
    ensure: res == balance
    def query(self)

The very first "ensure" specifies that an implementation provides a state preserving instance variable called “self.balance” and that its value is set to 0. The way to specify changes in state (here "self.balance") is shown in "withdraw" and "deposit". If there are no changes in state, "query" gives an example of that.

Now let us add an implementation fulfilling the contracts. It's quite straight forward.

class Account(object):
    ensure: self.balance == 0
    def __init__(self):
        self.balance = 0

    require: 0 < amount <= self.balance
    context: balance = self.balance
    ensure: self.balance == balance - amount
    def withdraw(self,amount):
        self.balance -= amount
        
    require: amount > 0
    context: balance = self.balance
    ensure: self.balance == balance + amount
    def deposit(self,amount):
        self.balance += amount
        
    context: balance = self.balance
    ensure: res == balance
    def query(self):
        return self.balance

Something is weird here: The implementation (4 lines) looks just like a reformulation of the “context” and “ensure” blocks (7 lines). In addition, the implementation is much more easier to grasp and to understand. No doubt, the contracts are way too heavy compared to the implementation. We could easily condense our specification if the implementation is regarded as part of the specification.

class Account(object):
    def __init__(self):
        self.balance = 0

    require: 0 < amount <= self.balance
    def withdraw(self,amount):
        self.balance -= amount

    require: amount > 0
    def deposit(self,amount):
        self.balance += amount

    def query(self):
        return self.balance

That's easy and lightweight, isn't it?

Things have become much more simpler, the code is definitely easier to read and to grasp. But is this still a specification? Yes, but the viewpoint has changed. Design by Contract is a technique, which tells you, whether an implementation fulfills the contracts or not. DbC cannot generate answers for you, it can just verify if your answer (an implementation) is valid or not. This is somewhat impractical if a state space needs to be maintained for DbC to verify an implementation; in some sense you’re doing double work. In a purist approach you would maintain independent state spaces: one for specification purposes and another for the implementation. An alternative style is to create an executable specification, which lets you experience the right answers by trying it out. It’s a way to show, what withdrawal, deposition etc. actually do, so that you can understand their behavior. In our example, we mixed both styles, taking advantage of each style, where it fits best.

If you write your code this way, you are coding a specification, which is executable. And that’s quite some fun. The risk is that you start to mix in implementation issues with an eye on performance, optimizations etc. You shouldn’t. You are writing a specification using your favorite programming language. That's it! No more, no less.