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.

Comments

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
Queue Testing  08 Dec 2018
Creating Branching Nodes  01 Dec 2018
Two Dual Item Queues  24 Nov 2018
Simple Queues  17 Nov 2018
Enqueuing Values  10 Nov 2018
Dequeuing Values  03 Nov 2018
Designing the External API  27 Oct 2018
Introducing the Priority Queue  20 Oct 2018
A better approach to reflection  13 Oct 2018
Avoiding Magic Strings  06 Oct 2018
More csharp posts »
Archives
April 2008
2008