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
Using Constructors  27 Feb 2023
An Inconvenient API  18 Feb 2023
Method Archetypes  11 Sep 2022
A bash puzzle, solved  02 Jul 2022
A bash puzzle  25 Jun 2022
Improve your troubleshooting by aggregating errors  11 Jun 2022
Improve your troubleshooting by wrapping errors  28 May 2022
Keep your promises  14 May 2022
When are you done?  18 Apr 2022
Fixing GitHub Authentication  28 Nov 2021
April 2008