I can haz spec# kthx

Greg Young has been talking about Spec# for a long time. I was skeptical. I was argumentative. I was interested in attending the Spec# talk at the Seattle Alt .Net open spaces. I was blind, but now I see.

DBC

DBC is Design By Contract. The Pragmatic Programmer dedicates a decent chunk of time to this concept (chapter 4, pp 109-119 in my copy) but I'm going to give a brief overview that will probably not be adequate to really explain it, but I hope it makes you want to go read about it.

The idea behind it is that it's hard to work with many different modules and their interactions with each other because invariably you'll make mistakes. In order to make this easier, you specify contracts that a module will abide by. These are defined by preconditions, postconditions, and invariants. A precondition is something that must be true in order for a module to do its job. It isn't user input validation, since the user might make mistakes. It's things that, if met, the object with them will guarantee a particular result. This result is defined by the postconditions. Invariants are things that may interact with that particular method but at the end of that method their conditions will be true, regardless of what may have happened during that method call. So here's an example:

Let's say that I have a method that searches a sorted array for a particular value. Preconditions would include:

1. The list must be sorted
2. The list object can never be null

Postconditions would be:

1. The output object will be the object that was searched for if found.
2. The ouptut object will be null if the input was not found.

Invariants might be:

1. The order of items in the list will not change
2. The list will never be null

So what does this mean in code? It means that in order for this method to be successful, I have to guarantee that the caller will sort the list first and that they'll NEVER pass a null object in the list. It also means that the search method will always return the object searched for or null if not found, and it will NEVER return anything else. Finally, it means that although the method may do things to the list while it executes, the list that exists after the method terminates will be identical to the list that was passed in (assuming you're passing the list by reference).

So how do you enforce this?

Short answer: you can't. The only thing you can do is to put Asserts on your contracts and let them fail if somehow your contract is not met. This means that somewhere, your code is not correct. These constraints define things that should NEVER happen. A breach of contract is NOT a bug, it's a part of your code that is incorrect and needs to be fixed. At runtime, it's possible that something totally messed up might occur, like something in your list getting overwritten due to a buffer overflow or getting an out-of-memory exception because Sql Server is consuming all of your available RAM (I've seen that happen). When that happens, your contracts will catch it and throw an exception with detailed error messages. That is, if you've left Asserts turned on in Release, which I know most of you don't. My lead would probably castrate me if I suggested this.

Enter The Dragon (where Dragon = Spec#)

Spec# allows you to explicitly define contracts in your code that are then checked at compile time (this is optional). You can also add invariant constraints to your properties and such. You can add preconditions and postconditions. This does a few things for you:

1. Spec# sets up checks for violations of your contracts at runtime. It will automatically throw exceptions for you if they are violated, so no more checking if an object is null, just put a precondition on it.
   
2. There is static code verification that analyzes your code to see if you are ever potentially violating your contracts. It will actually throw a compile error if you might be writing incorrect code (this is an option that you can disable though).

The halting problem

So, like me, you might have said "Well, what about the halting problem? It's provably true that you can never write a program to analyze another program to determine if it will ever halt. What about that, huh? How do you get around that? Look at me, I know Computer Science buzzwords even if I can never actually show you the proof of that problem or illustrate it on a Turing machine or anything. I don't know what a Turing machine is but I read about it in Cryptonomicon and it makes me sound smart."

Well, that isn't a problem because the static verification will only prove your program under certain conditions. There are methods that are too complex to prove, or conditions under which a proof is impossible. To help this, you get the "Assume" keyword which allows you to set assumptions about the circumstances of your methods so that static verification can try to prove it, but this may still break something (although your contracts should still catch this at runtime).

In conclusion

Go download spec# and see how awesome it is. Then email microsoft and tell them to release it as a product. I told Scott Hanselman that if he blogged about it, and I blogged about it, then the 30,000 people who read his blog will all email Microsoft about it and the eight or so people who read my blog will also email Microsoft about it and then they'll have 30,008 emails demanding Spec# and we'll get it released.