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.


blog comments powered by Disqus
Next Post
The Gray Zone  04 May 2008
Prior Post
Configuration Manager in Visual Studio Express  25 Apr 2008
Related Posts
When (not) to use Var  16 Jul 2016
Semantic Types Redux  05 Jun 2016
Semantic Types in C#6  27 May 2016
Property Enhancements for C#  20 Dec 2015
Language Extensions for C#  19 May 2014
When should methods be Static?  09 Oct 2012
Of Method Naming and more  29 Sep 2012
Someone needs an intervention  16 Dec 2011
CallerInfo in C# 5  08 Dec 2011
Regions in C#  16 May 2011
More csharp posts »
Related Pages
April 2008 archive