Statically checked design by contract

Question

I recently got excited by the idea of statically check design by contract in .net 4.0 / Visual Studio 2010.

However I was saddened to find out that it will only be available in Visual Studio Team System. http://msdn.microsoft.com/en-us/devlabs/dd491992.aspx

Are there any alternatives which give statically checked design by contract for c#?

Will the mono project be adding this functaionality to there compiler?

Answer 1

Code contracts do not require the C# compiler as they are implemented as classes in the .NET Framework 4.0. Any .NET compiler that can emit a managed assembly is usable, although C++/CLI will likely emit an incompatible assembly when mixing managed and native code.

There are additional tools executed by the IDE to rewrite the resulting IL so that the contracts appear in the correct location, and thus the Mono project authors would need to write similar tools for contracts to work on the Mono platform.

See this post for more information.

Answer 2

He's referring to the theorem prover.

There's nothing stopping the open-source or commercial community from implementing their own. The Contracts classes are part of the BCL and trivially easy to add to, say, Mono. "We'll" need to make a theorem prover if we want to statically check things.

The prover is not part of the compiler. It basically runs as follows:

• Compile a version of the binary with CONTRACTS_FULL defined. This emits all Contract attributes and calls to the Contract class static methods.
• Load the assembly "for reflection only," and parse all the method's byte code. A detailed flow analysis with state information will allow certain contracts to be shown "always true." Some will be "known false at some point." Others will be "unable to statically prove the contract."

As the tool gets better, it will go from giving warnings about every contract to eventually offering similar proving results to the Microsoft version.

Edit: Man, if Reflector was open sourced it would be great for this. A first-pass implementation could certainly operate as a plugin. That way the prover logic can be designed without worrying about how the binaries are loaded. Once it proves functional (get it?), the logic could be extracted and built to operate on the syntax trees produced by another assembly loader (one that is open source). The important/novel thing here is the prover logic - the assembly loader has been done multiple times and nothing changes spectacularly for this use.