Design by Contract, by Example

Posted on November 19, 2012



I read this book prior to my last trip to Japan (2011), and I took me several weeks to go through it. I can say without hesitation that I wish I had seen it at the start of my career.

You should really buy this book

You should really buy this book

Using concrete, non-trivial examples based on use cases that working developers can relate to (shipping services for example), Richard Mitchell and Jim McKim manage to describe what it means to develop a sufficiently correct and formal class model using Bertrand Meyer’s Design by Contract techniques.

Before I mention the contents of this book, allow me to deviate a bit into the theoretical. One awfully underutilized and misunderstood principle in software is the guaranteeing of program correctness. The essence of program correctness can be explored (among many ways) by using Hoare triples in Hoare’s logic of programs.

Logical formulas of the form {P^I}C{Q^I} describe what it means for a piece of code “C” to execute correctly under a given context. Unfortunately, when we get to learn about these techniques in college, we typically get trivial examples that do not elaborate the true usefulness of such constructs.

Gee, I proved that if i = 1, after adding 1 to it, then i = 2. Somebody gimme a cookie!!!

What an awful way to present such seminal work!!! This is where, in my opinion, Mitchell and McKim’s book truly shines.
Their book provides real-world examples that showcase the idea of behavior preservation and inheritance, and not just structure inheritance. Not only that, it does explain in practical terms what it means (or it should mean) for a class to be a sub-type of another.

In doing so, they present a direct and practical, real-life connection between day-to-day software development with design by contracts. This leads to behavior preservation and behavior inheritance.

Use The Source Luke!

The beauty of this is that this is within the reach of day-to-day programmers. The techniques rarely (if ever) require any delving into CS theory or mathematical logic.  Additionally, neither do they require the use of a specialized language with DbC support such as Eiffel, nor does the day-to-day programmer need have access to some DbC pre-processor or use compiler-specific pragmas.

Instead, it relies in good old rules of thumb and guidelines on how to structure software. The technique simply employs tried-and-true quality software techniques in a manner that is methodical and aimed at inheriting and preserving behavioral guarantees.

The book neatly ties the logical formulas of Hoare triples, the contracts these represent, and behavioral sub-typing (as described in Barbara Liskov’s seminal works). That is, the book prescribes methodical steps by which good class models can usefully constructed, and prescribes a notion of re-usability and composition in terms of contracts.

What I really like about this book (and the reason I wish I’ve had it before) is that it provides a revelation – a class “extending” a super class is not really an extension in terms of usage. In terms of additional features and refinements, it might be an extension.

But in terms of usage, a subclass is a restriction of a super class. A properly constructed subclass is one with its use cases being a subclass of its superclass’ valid use cases.

A function A can replace another function B if A retains or weakens B’s preconditions and strengthens B’s post conditions. Ergo the cases where A can be used are a subset of the cases B can be used. Inductively, then, a class X is the sum of its methods, and the complete context in which such a class can be used is the sum of its pre-conditions and post-conditions.

And if that is the case, then a class X sub-classing class Y presents a context narrower than the context in which Y can be used. This is a very, very powerful concept. It provides a way to measure if a given class design is sound or not.

This is a book that I strongly recommend for anyone who wants to take their OOA/OOD skills to the next level.