Direkt zum Hauptbereich

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.

Beliebte Posts aus diesem Blog

Lidl und der Kassen-Bug

Es gibt Fehler, im Informatiker-Jargon "Bugs", die etwas anrühriges haben. Ich bat den Menschen an der Kasse bei Lidl um einen Moment Geduld und meine Kinder um Ruhe, um nicht den wunderbaren Moment zu verpassen, bei dem es passierte. Der Lidl-Mensch fluchte kurz auf -- und ich war entzückt! "Einen Moment, davon muss ich ein Foto machen!" Und dann machte ich noch eines. Ich bin heute extra für diesen Fehler zu Lidl gepilgert -- ich wollte es mit eigenen Augen sehen. Gestern hat mir ein Student (vielen Dank Herr Breyer) von diesem Fehler in einer EMail berichtet. Ein richtig schöner Fehler, ein Klassiker geradezu. Ein Fehler, den man selten zu Gesicht bekommt, so einer mit Museumswert. Dafür wäre ich sogar noch weiter gereist als bis zum nächsten Lidl. Der Fehler tritt auf, wenn Sie an der Kasse Waren im Wert von 0 Euro (Null Euro) bezahlen. Dann streikt das System. Die kurze Einkaufsliste dazu: Geben Sie zwei Pfandflaschen zurück und Lidl steht mit 50 Cent bei Ihne

Syntax und Semantik

Was ist Syntax, was ist Semantik? Diese zwei Begriffe beschäftigen mich immer wieder, siehe zum Beispiel auch " Uniform Syntax " (23. Feb. 2007). Beide Begriffe spielen eine entscheidende Rolle bei jeder Art von maschinell-verarbeitbarer Sprache. Vom Dritten im Bunde, der Pragmatik, will ich an dieser Stelle ganz absehen. Die Syntax bezieht sich auf die Form und die Struktur von Zeichen in einer Sprache, ohne auf die Bedeutung der verwendeten Zeichen in den Formen und Strukturen einzugehen. Syntaktisch korrekte Ausdrücke werden auch als "wohlgeformt" ( well-formed ) bezeichnet. Die Semantik befasst sich mit der Bedeutung syntaktisch korrekter Zeichenfolgen einer Sprache. Im Zusammenhang mit Programmiersprachen bedeutet Semantik die Beschreibung des Verhaltens, das mit einer Interpretation (Auslegung) eines syntaktisch korrekten Ausdrucks verbunden ist. [Die obigen Begriffserläuterungen sind angelehnt an das Buch von Kenneth Slonneger und Barry L. Kurtz: Formal Syn

Mit Prof. Handke im Gespräch: Vom Workbook zum Inverted Classroom

Aus dem Netz in Handkes Büro Es gibt diese schönen Momente, da führen soziale Medien zu sozialen Begegnungen im echten Leben. Ich twittere im Nachgang zur #BiDiWe16, ein Dialog mit Jürgen Handke ergibt sich, er schickt mir seine Telefonnummer, ich rufe sofort durch, wir verabreden uns. Drei Tage nach der #BiDiWe16 sitze ich bei Handke im Büro, das gleichzeitig sein beachtlich ausgestattetes Aufnahmestudio beherbergt. Es ist Freitagmorgen, 9. September 2016. Jürgen Handke ist mir kein Fremder. Ich habe zwei seiner ICM-Konferenzen besucht, auf der #BiDiWe16 in Berlin hielt er die Keynote. Er hat für seine Lehre Preise erhalten, zuletzt 2015 den Ars Legendi-Preis für exzellente Hochschullehre. Zugegeben, ich hadere mit dem Konzept des Inverted Classroom -- auch Flipped Classroom genannt. Meine Erfahrungen mit der Programmierausbildung von Informatik-Studierenden des 1. und 2. Semesters lassen mich zweifeln. Videos habe ich auch schon produziert, aber vor allem das selbstgesteuerte