Spec# in the Real World

Now that I have the time for it, I’m going through a lot of material I’ve been collecting in my To Read folder over the past year or so. One of the videos I watched is Mike Barnett’s talk about Spec# at the recent Lang.NET Symposium.

What Spec# does, in a few words, is to add contracts to your code: Your method never returns null? Set this as a contract and everyone calling your method could rely on this; Should you always receive a number between x and y into a certain parameter? Set this as a contract and no one can call your method before their code explictly shows that the parameter is between those boundries.

Except for the fact that it shows some awesome concepts in keeping everything nice, clean and also reduces the amount of unit testing required by using these contracts, it made me say “woah, I didn’t even think of that,” when the squiggly lines started appearing in places I hadn’t expected (yes, it works in the background and shows you problems as you code). However, I can’t seem to stop thinking that Spec# has one huge fault: Out of all of the developers I have ever worked with, about 90% will never use it unless they are forced too, which is sad. I feel this is going the way of checked exceptions in Java, where the functionality is there and is great when used, but most people just don’t use it because it’s less work and the code still works.

I, for one, would love to see Spec# embedded into C# 4.0 (my guess is it won’t be ready for 3.0), after the syntax is cleaned up a bit. I think it’s a great and welcome step forward in code-hardening, but its biggest problem is how to make Spec# such an integral part of C# so that it doesn’t follow the footsteps of other great software features no one ever uses.

Advertisements

5 thoughts on “Spec# in the Real World

  1. Even if a developer does not write the “specs” for their methods, Spec# can still check that any code they write keeps to the “specs” for the framework’s methods. It would be possible in a lot of cases for the Spec# compiler to work our the preconditions for methods it’s self anyway.  I would like to see ALL of the .NET framework methods have the “specs” written for them, and then the C# compiler check against these specs, but only give a warning as standard rather then an error. When will the c# compiler trap simple error like this: private string name; public string Name {    get{return Name;} }

  2. There is some hope, fortunately, and that hope is that many of the Spec# contracts are like C const function parameters: once you start using them, it's viral; calling code is forced to use them or get an error/warning. I think even if few people used it in their assemblies, you could at least use it in your own, verifying that your code is truely solid. And with the ability to add out-of-band contracts to assemblies you don't have the source to, you can truely ensure your assembly is rock solid.

  3. The problem is that even if you use assemblies using contracts, you still only have to fulfill the contracts you call and not create contracts of your own, making only your outgoing calls solid, but not you self calls between bits of your own code.
    I have no doubt in my mind that when Spec# is out of research and is out into the big world that I will be one of the first ones to use it :)

  4. Just a quick thought, but when C# first came out, one of the "features" (or lack thereof) that I was glad to see was that the throws clause from Java was gone.  And that seemed to me like a decision made from experience.  In the real world, the requirement was just so easily circumvented (throws Exception), or the even worse wrap-and-rethrow mess, that the purist ideal was just too easily lost. So I'd hope that Spec# builds flexibility into itself.  The ability to turn the features on and off, and to interact meaningfully and cleanly with code that doesn't follow contracts as explicitly. I can't help but be reminded, though, of the relative fizzle in the widespread use of mathematically proven algorithm libraries.  It seems that developers would much rather go with something that has been tested by popular use. But being able to build into the signature of a method things that I would otherwise Assert() seems quite useful.  Off to read up more about it.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s