Statically tested design by contract

Question

Recently, I was delighted with the idea of ​​statically checking design by contract in .net 4.0 / Visual Studio 2010.

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

Are there any alternatives that give a statically tested contract design for C #?

Will a monoproject add this functionality to the compiler?

Answer 1

He means the proof of the theorem.

There is nothing stopping the implementation of an open or commercial community on their own. Contract classes are part of BCL and it is trivially easy to add, say, to Mono. "We need to make a theoretical breakthrough if we want to statically check things.

This tool is not part of the compiler. It basically works as follows:

• Compile the binary version with CONTRACTS_FULL . This emits all the attributes of the Contract and calls to the static methods of the Contract class.
• Download the reflection-only assembly and parse the entire method byte code. A detailed analysis of the flow with status information will allow certain contracts to be shown “always true”. Some of them will be “known at some point”. Others will be "unable to statically prove the contract."

As the tool improves, it will give warnings about each contract in order to ultimately offer similar results to the Microsoft version.

Edit: Man, if Reflector was open, that would be great for that. The implementation of the first pass, of course, can work as a plugin. In this way, the validation logic can be constructed without worrying about how binary files are loaded. Once it turns out to be functional (get it?), Logic can be extracted and built to work with syntax trees created by another assembly loader (which is open source). An important / new thing here is the validation logic - the assembly loader has been done several times, and nothing has changed spectacularly for this use.

Answer 2

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

The IDE has additional tools to rewrite the received IL so that the contracts appear in the right place, and thus, the authors of the Mono project needed to write similar tools for contracts for working on the Mono platform.

See this post for more details.