Dienstag, April 10, 2007

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.

1 Kommentar:

Aaron Mueller hat gesagt…

On simple methods, it's a pragmatic technique to validate the written code, but on more complex things like parsing syntax or handling with files, the implementation mixes (imho) too much with the specification. It's hard to read out the specification from a source-file (sure, not in the Account-example). So why putting specification and source-code together at all?

UnitTests separate validation-checks ("specification") and implementation in two separate files. Behavior-Specification (http://blog.datenhalter.de/?p=48, http://rspec.rubyforge.org/) has a similar approach. On these behavior-tests (and traditional UnitTests) there are no need for the "context state-variable" because the test instantiate a new object from the class and access the needed value from an attribute in the state, when the test needs them.

Why do you prefer pre/post-conditions for specification?

Greetings,
Aaron
(sorry for my bad englisch)