Scott Hanselman talks to the spec# team at Microsoft.
What is spec#? It sits ontop of C# and according to its website provides:
“The Spec# programming language. Spec# is an extension of the object-oriented language C#. It extends the type system to include non-null types and checked exceptions. It provides method contracts in the form of pre- and postconditions as well as object invariants.
The Spec# compiler. Integrated into the Microsoft Visual Studio development environment for the .NET platform, the compiler statically enforces non-null types, emits run-time checks for method contracts and invariants, and records the contracts as metadata for consumption by downstream tools.
The Spec# static program verifier. This component (codenamed Boogie) generates logical verification conditions from a Spec# program. Internally, it uses an automatic theorem prover that analyzes the verification conditions to prove the correctness of the program or find errors in it.
A unique feature of the Spec# programming system is its guarantee of maintaining invariants in object-oriented programs in the presence of callbacks, threads, and inter-object relationships.”
Here’s an overview in PDF form.
I haven’t taken more than a couple minutes to see what spec# is, but I can see where the general idea of programming by contract is a reasonable one for some cases. Is this implementation discoverable and valuable enough not only to the human, but the computer? I’m not so sure. Worth checking into.
[Found via thred.com\msdev]
