Design-By-Contract with Spec#

I was reading Billy McCafferty’s introduction to design-by-contract (DBC) and stumbled upon Spec# which extends C# to support contracts in the form of object invariants, pre- and postconditions, throws sets; non-null types, etc. Microsoft Research has a great intro whitepaper, The Spec# Programming System: An Overview (PDF) which is definitely worth reading if DBC is of any interest to you.

Then Don (yes, he does have a last name) pointed me to a Dot Net Rocks episode with Rustan Leino who went over the specifics of the Spec# language, its compiler and the static verifier called Boogie. As far as I can tell, Spec# does some mind boggling things. I hope it gets baked into the language at some point in the future to further encourage development discipline.

Related reading

Design by contract at Wikipedia. The Martin duo also talk about it in their book.