InfiniTec - Henning Krauses Blog

Don't adjust your mind - it's reality that is malfunctioning

Using Code Contracts Visual Studio and with Resharper

CodeContracts are a new feature to write assumptions in .NET programs. A version for .NET 3.5 is available from the Microsoft Code Contracts. With .NET 4 they are part of the BCL. Unfortunately, they do nothing out of the box – a binary rewriter is required to enable runtime checking. The rewriter is also available from the Microsoft site specified above.

Enabling Code Contracts

Once the Code Contracts are installed on a machine, they must be enabled in each Visual Studio project by specifying the CONTRACTS_FULL conditional compilation symbol in the properties of a project:

ConditionalSymbol

Next, enable the runtime checking on the Code Analysis tab:

EnableRuntimeChecking

Now you can use the Code Contracts within the project. Here is a small sample application:

using System;
using System.Diagnostics.Contracts;

namespace SampleApplication
{
    internal class Program
    {
        public static int Divide(int a, int b)
        {
            Contract.Requires(b != 0);
            Contract.Ensures(a != 0 ? Contract.Result<int>() != 0 : Contract.Result<int>() == 0);

            return a/b;
        }

        private static void Main()
        {
            Console.Out.WriteLine("Divide(4, 2) = {0}", Divide(2, 2));
            Console.Out.WriteLine("Divide(4, 0) = {0}", Divide(4, 0));
        }
    }
}

It’s just a small division method which has one pre- and one post-condition: The method requires b not to be 0. The post-condition specifies that the result of the method is 0 if a is 0 and not 0 when a is not 0. Very simple. If you run the program, it will throw an exception on the second execution of the Divide method, because b is 0 in this case:

Precondition faileed

Integration with Resharper

If you are using Resharper, you are accustomed to the null-reference checking the tool performs as you type. This is quite handy to spot null-references during design-time vs. run-time.

Here is another method which is annotated with code contracts:

 

NullReference

Notice the squiggles under the name variable and the hint to a System.NullReferenceException. If you would replace the first line of the method with a

if (string.IsNullOrEmpty(name)) throw new ArgumentNullException("name");

the warning would be gone, because Resharper would sense that the code path with the if-statement is never executed if name is null.

To enabled this feature with Code Contracts, a file with certain annotations must be placed in the directory C:\Program Files\JetBrains\ReSharper\v5.1\Bin\ExternalAnnotations\mscorlib (C:\Program Files (x86)\JetBrains\ReSharper\v5.1\Bin\ExternalAnnotations\mscorlib on x64 systems). The file is attached at the end of this post.

Visual Studio Editor Code Contracts extension

A Visual Studio extension is available from the Code Contracts team. It can be downloaded via the Extension Manager. It visualizes code contracts directly in the editor.

image

Credits

The Microsoft.CodeContracts.xml is taken from a Youtrack issue http://youtrack.jetbrains.net/issue/RSRP-190566. I’ve modified the file to work with .NET 4.0.

Downloads


Posted by Henning Krause on Thursday, November 18, 2010 5:07 PM, last modified on Thursday, November 25, 2010 5:08 PM
Permalink | Post RSSRSS comment feed