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
Short-circuiting validation  11 Aug 2018
Aggregation of validation  04 Aug 2018
Recovery of validation types  28 Jul 2018
Basic validation  21 Jul 2018
Why we need better validation  07 Jul 2018
A question of struct performance  30 Jun 2018
Equality has Symmetry  17 Mar 2018
Type Miscellany  05 Mar 2017
Testing Immutable Types  25 Feb 2017
Factory Methods  18 Feb 2017
More csharp posts »
Archives
April 2008
2008