Exploring the .NET CoreFX Part 11: Code Contracts

This is part 11 of my Exploring the .NET CoreFX Series.

In 2008, Microsoft Research published Code Contracts, which provide a language-agnostic way to express coding assumptions in .NET programs. The assumptions take the form of pre-conditions, post-conditions, and object invariants.

Here is a simple example of code which uses Code Contracts:

using System.Diagnostics.Contracts;

public class StringUtils
{
    internal static string Append(string s1, string s2)
    {
        Contract.Requires(s1 != null);
        Contract.Requires(s2 != null);
        Contract.Ensures(Contract.Result<string>() != null);
        return s1 + s2;
    }
}

Code Contracts assertions are not limited to runtime enforcement. They may instead be enforced by compile-time static analysis. For example, it is very simple to annotate methods with Code Contracts, set up a continuous integration (CI) server to perform static analysis, and fail the build if there are any failed assertions. This gives us the best of both worlds: a guarantee our code enforces our assumptions with essentially zero runtime penalty.

By design, Code Contracts are not enforced unless the appropriate tools are configured to check them. For this reason they are usually not appropriate for parameter validation on public methods; there is still the need for traditional parameter validation. However you can combine traditional parameter validation on public methods with Code Contract-based assertions for internal methods as follows:

public class StringUtils
{
    // This is the method that external callers would use, as we can't
    // guarantee they will enforce Code Contract checking
    public static string Append(string s1, string s2)
    {
        if (s1 == null)
            throw new ArgumentNullException("s1");
        if (s2 == null)
            throw new ArgumentNullException("s2");
        // The Code Contracts static analyzer is quite clever and it
        // realizes that the AppendInternal pre-conditions are satisfied
        // due to the above two statements, so no Contract.Assert()s
        // are required.
        return AppendInternal(s1, s2);
    }

    // This is the method that other code in this assembly would use,
    // as we can guarantee that this code is checked at compile-time
    // with the Code Contracts static analyzer
    internal static string AppendInternal(string s1, string s2)
    {
        Contract.Requires(s1 != null);
        Contract.Requires(s2 != null);
        Contract.Ensures(Contract.Result<string>() != null);
        return s1 + s2;
    }
}

You can write Code Contracts assertions with just the .NET 4.5 SDK installed, but they will not be enforced. To enforce them at compile-time within Visual Studio:

  1. Install the Code Contracts for .NET extension using NuGet: Code Contracts
  2. Restart Visual Studio
  3. Open up the Project Properties dialog and click on the Code Contracts tab
  4. Click “Perform Static Contract Checking” Code Contracts Project Properties

System.Collections.Immutable uses Code Contracts only to express post-conditions and object invariants, never to validate pre-conditions. This is presumably to integrate well with client code which uses Code Contracts.

For more information on Microsoft Code Contracts, please read:

Recommendations

  1. Liberally annotate all methods with Code Contracts post-conditions and object invariants.
  2. If you can guarantee that a method will be called only by code that you control (e.g. internal methods), use Code Contracts to enforce pre-conditions. If you cannot, use traditional parameter validation.
  3. Integrate Code Contracts static code analysis into your CI pipeline, and fail the build on any warnings.