A great many years ago I was fascinated by Bertrand Meyer’s book “Object Oriented Program Construction.” One of the many remarkable things in that book is the idea of “Design By Contract”, where you specify what a method does by means of a logical pre– and post–condicion. Consider the square root function:
pre: x ≥ 0 post: abs(y*y - x) < epsilon
This is a very good specification:
- It’s efficiently executable.
- The intent is clear.
- Gives no hint about how to implement it, i.e., it does not contain design ideas.
Now I’m reading the Scrumban book by Corey Ladas. One thing Corey says is that Test-Driven Development is good, but not as good as Design By Contract; in fact, he says, TDD might be a stepping stone to DBC.
I have never met someone who does DBC. This by itself does not mean a lot, as I’m not widely travelled, in working experience. I’d be quite interested in reading experiences about this. Anyway I suspect that there are fundamental reasons why it’s not widely practiced. My hypothesis is that the square root is an exceptionally good DBC example, but most functions are not as easily specified by contract.
Consider for example the function “specified” by the following TDD-style tests:
it "returns empty string for empty string" do assert_equal "", squeeze("") end it "replaces sequences of equal characters with one" do assert_equal "abca", squeeze("aaabbccccaa") end
I think it’s quite clear how we should implement this function, even though we are given just two examples of its behaviour. How would we specify it with DBC? I’m not sure what is the best way. I thought about this for a long time (believe me) and this is the best I came up with:
pre: true // any string is valid input post: let s be the input string. let s' the output string. (∀ i: s'[i-1] ≠ s'[i]) ∧ (∀ i,j: i < j ⇒ (∃ k,l: k < l ∧ s'[i] = s[k] ∧ s'[j] = s[l] )) )
You read it like this:
- The output string does not contain consecutive equal values (that was easy!)
- Two distinct values in the output string must have been present in the input string and in the same order.
Now is this a correct specification? Can I *prove* that this specification is correct? Well, this is a specification, so it’s supposed to be self-evidently correct. But is it? I don’t think it is self evident at all. I think it takes a bit of thought to understand it. It’s not easy to find a way to prove it correct. One way is to look for counterexamples, that is, find a pair (s,s’) that satisfies the specification yet contradicts my intuitive notion of what “squeeze” should do. (In fact, I can think of at least two examples that prove that this specification has holes. Can you find them?) In other words, it turns out that the only way to convince myself that this specification is correct is by testing it on carefully chosen examples!
Well it’s not true that I can’t find a clearer specification. Consider this other one:
pre: true post: let squeeze behave like f where f() =  f([x]) = [x] f([x,x|rest]) = f([x|rest]) f([x,y|rest]) = x + f([y|rest]) if x ≠ y
The notation [x,y|rest] means “a string that begins with character x, then character y, then 0 or more other characters.” My observations follow.
This is a purely mathematical specification of function squeeze, as pure as the previous one. It’s arguably clearer than the previous specification. I think this one is correct. I could test it against a few cases just to make sure, but it seems OK to me.
This spec can be executed efficiently, while checking an input-output pair against the other spec requires quadratic time.
But there’s a problem; this spec is actually a program. Once I have this spec I can use *this* for an implementation and work no more. I already have my implementation.
In conclusion, this is my objection to DBC: I suspect that the square root is an exception; most methods are too complex to specify with pure logic, or require us to write a functional program that solves the problem. In both cases we are left with the need to test our specification on specific examples.
This is why I think TDD is for most purposes more effective than DBC. In general, concrete examples are by orders of magnitude simpler to write and more self-evident than universal statements. Most universal statements will have to be tested against examples anyway, or we wouldn’t be confident in their correctness.
Long live examples!