Spec#

Spec# is a C# based language from Microsoft Research. It extends the language by adding comprehensive support for Contract Based Programming, with new keywords such as assume, require and expose.

While the ideas behind contract based programming aren’t new (Bertrand Meyer based the Eiffel programming language around the ideas in the late 1990’s), Spec# brings many of the ideas to the world of .NET.

One feature implemented by Spec# that is quite interesting is the static analysis that becomes possible -a static verifier can pick up on the preconditions, postconditions, invariants and other constraints that you declare in your code and check to see if they are satisfied or not. This provides a powerful mechanism for validating that your code works as you intend, as the static verifier covers all possible execution paths.

Of course, every tool has a downside. In the case of Spec#, I see two significant ones - one an accident of implementation (and therefore reversible), the other a side effect of the approach.

First the reversible problem: the current edition of Spec# is a custom built compiler based on the C# 2.0 language - so, while you get all the Design by Contract goodness of Spec#, you lose LINQ and all its related goodness. If we’re lucky enough to see the ideas of Spec# rolled into the next edition of C#, this problem will go away.

The second issue is, I believe, more serious.

I believe the additional power we gain from the precepts of Design by Contract is considerable - allowing some developers to deliver more complex and more reliable systems faster than before.

However, the level of talent and skill required of developers is higher as well.

Contract based programming is inherently more methodical, more intentional and more deliberate. Simply expressing the preconditions and postconditions for a simple method requires a nontrivial amount additional thought. Further, it requires additional skills that many developers would need to learn.

Consider: There are a lot of developers out in the ‘real world’ who couldn’t care less about the theoretical aspects or niceties of the code they write. Often, these developers don’t have a job title of ‘Programmer’ or ‘Developer’ - they are business people who have just enough skill to write code to make their job easier.

These business-developers are the people who most need some kind of electronic coach to watch over their shoulder and help them write code that works, yet they’re also the people least likely to understand or use Design by Contract.

Don’t get me wrong - I think Spec# is a great language, and the work that’s been done by this team is spectacular. I just think that it is a long way from being ready for prime-time use by a regular Joe programmer.