---

May 2011

Volume 26 Number 05

Cutting Edge - Code Contracts Settings in Visual Studio 2010

By Dino Esposito | May 2011

Last month I introduced software contracts as they’re implemented in the Microsoft .NET Framework 4. Known as Code Contracts, software contracts allow you to express formal conditions your code should fulfill to work properly. Code Contracts cause your code to throw an exception if a method doesn’t receive data as expected or if it produces data not following expected postconditions. For an overview of preconditions and postconditions, you might want to check out my article in last month’s issue (msdn.microsoft.com/magazine/gg983479).

Code Contracts are part of the .NET Framework 4, but also rely on a few facilities in Visual Studio 2010, such as runtime tools, integration with MSBuild and a property page in the Project Properties box. It’s important to note that just writing preconditions and postconditions is not enough. You also need to turn on runtime checking capabilities for each project to enjoy software contracts. You do that through the Code Contracts project property page in Visual Studio 2010. 

In this article, I’ll discuss the intended purpose of the various options you can check or select and drill down into the rewriter tool and practices for the most common thing you do with Code Contracts: argument validation.

The Code Contracts Property Page

Should Code Contract preconditions and postconditions be enforced in all builds or only in debug builds? In practice it comes down to your conception of a software contract. Is it part of the design effort? Or is it just a debugging measure?

If it’s a design function, then there’s no reason to strip out Contracts in release builds. If it’s just a debugging technique, then you don’t want to have it around when you compile in release mode.

In the .NET Framework, Code Contracts are just a part of the framework and are not baked into any of the languages. As a result, it’s easier to configure them on a per-build basis within your project. The .NET Framework implementation of software contracts therefore leaves it up to you to decide where and when it’s appropriate to implement the Contracts.

Figure 1 shows the property page in Visual Studio 2010 through which you set up how you want software contracts to work for an application. Note that such settings apply on a per-project basis and therefore can be adapted as appropriate.

Figure 1 The Property Page for Code Contracts in Visual Studio 2010

You can select the configuration of choice (Debug, Release and so on) and apply settings only to that configuration. In this way, you can enable Code Contracts for debug, but not for release and, more importantly, you can reverse the decision at any time.

Runtime Checking

To enable Code Contracts you must check the Perform Runtime Contract Checking option. If you leave that unchecked, then any Contract instructions you may have around the source code will produce no effect (except for Contract.Assert and Contract.Assume in any build where the DEBUG symbol is defined, but that’s sort of a minor point). The checkbox controls whether the rewriter tool is triggered at the end of each compile step. The rewriter is an external tool that post-processes software contracts and modifies the MSIL code, placing precondition, postcondition and invariant checks in the right places.

Note, however, that if you have a precondition like this, you’re going to get a runtime assert failure if you keep the rewriter off:

Contract.Requires<TException>(condition)

Figure 2 shows the message box you get.

Figure 2 The Code Requires Runtime Contract Checking

To see how runtime checking works in detail, consider the following code:

public Int32 Sum(Int32 x, Int32 y) {
  // Check input values
  ValidateOperands(x, y);
  ValidateResult();

  // Perform the operation
  if (x == y)
    return 2 * x; 
  return x + y;
}

The contract details are stored in the ValidateXxx methods using ContractAbbreviators as discussed in last month’s column. Here’s the source code for ValidateXxx methods:

[ContractAbbreviator]
private void ValidateOperands(Int32 x, Int32 y) {
  Contract.Requires(x >= 0 && y >= 0);
}

[ContractAbbreviator]
private void ValidateResult() {
  Contract.Ensures(Contract.Result<Int32>() >= 0);
}

If you use Contract.Requires instead of Contract.Requires<TException>, then you save yourself from the failure of Figure 2 if you keep the rewriter off in one of the builds. The message box in Figure 2 is due to the internal implementation of  Contract.Requires, which looks like this:

[Conditional("CONTRACTS_FULL")]
public static void Requires(bool condition, string userMessage) {
  AssertMustUseRewriter(
    ContractFailureKind.Precondition, "Requires");
}

public static void Requires<TException>(bool condition) 
  where TException: Exception {
  AssertMustUseRewriter(
    ContractFailureKind.Precondition, "Requires<TException>");
}

The Conditional attribute indicates to compilers that such a method call should be ignored unless the CONTRACTS_FULL symbol is defined. This symbol is defined only when you turn on the Perform Runtime Contract Checking option. Because Contract.Requires<TException> is not conditionally defined and lacks the attribute, the rewriter check is performed and results in a failed assertion if runtime Contract checking is disabled.

Let’s move ahead and consider the effect of using the rewriter on the previous code. You can easily verify for yourself what I’m saying by just using breakpoints and hitting Ctrl+F11 to bring up the Disassembly view in Visual Studio 2010. Figure 3 shows the content of the Disassembly view when you step through the method Sum compiled without enabling runtime Contract checking. As you can see, the source code is the same as you wrote in the class.

Figure 3 Disassembly View Without Runtime Contract Checking

When you enable runtime checking, the rewriter tool passes over the compiler returns and edits the MSIL code. If you step through the same code with Code Contracts enabled, you see something like Figure 4.

Figure 4 Postconditions Checked Past the Return Statement

The notable difference is that ValidateResult is invoked right before exiting the Sum method and past the return statement. You don’t have to be an MSIL guru to read what’s going on in the code in Figure 4. Operands are validated before the method starts honoring the topmost position of preconditions. The code that contains postconditions is moved to the bottom of the method and the MSIL code for the final return statement just falls into it. More interestingly, the first return statement—the one that in the Sum method implements a shortcut—now just jumps to the address where ValidateResult begins:

...
           return 2 * x;
00000054  mov         eax,dword ptr [ebp-8]
00000057  add         eax,eax
00000059  mov         dword ptr [ebp-0Ch],eax
0000005c  nop
0000005d  jmp         0000006B
...
            ValidateResult();
0000006b  push        dword ptr ds:[02C32098h]
...

Going back to Figure 1, notice the drop-down list near the Perform Runtime Contract Checking checkbox. That list lets you indicate the number of software contracts you want to enable. There are various levels: Full, Pre and Post, Preconditions, ReleaseRequires and None.

Full means that all types of software contracts are supported and None means that none of them are taken into account. Pre and Post excludes invariants. Preconditions also excludes Ensures statements.

ReleaseRequires doesn’t support the Contract.Requires method and only allows you to specify preconditions using Requires<TException> or the legacy If-Then-Throw format.

The Project Property page allows you to enable or disable runtime checking on a per-project basis, but what if you want to disable runtime checking only on a few sections of your code? In that case you can just disable runtime checking programmatically using the ContractRuntimeIgnored attribute. However, a more recent release (1.4.40307.0) added a new Skip Quantifiers option that also allows you to not execute any contracts that contain references to Contract.ForAll or Contract.Exists.

You can apply the attribute to members you use in Contract expressions. If the member is decorated with the attribute then the entire Contract statement in which it appears is not subjected to runtime checking. The attribute is not recognized in Contract methods such as Assert and Assume.

Assembly Mode

The Code Contracts properties also let you configure an Assembly Mode setting for the Contracts. The setting refers to how you intend to perform argument validation. There are two possible options: Standard Contract Requires and Contract Reference Assembly. The Assembly Mode settings help tools like the rewriter to fine-tune the code and give proper warnings when necessary. Let’s say that you use the Assembly Mode to declare your intended use of Code Contracts for parameter validation. The Assembly Mode settings introduce a couple of simple rules you must fulfill, otherwise you’ll get a compile error.

Assembly Mode should be set to Standard Contract Requires if you use methods Requires and Requires<T> to validate method arguments. You should use Custom Parameter Validation if you use any If-Then-Throw statement as preconditions. If you don’t use  Custom Parameter Validation, the statement will be treated like a Requires<T>. The combination of Custom Parameter Validation and explicit use of any form of Requires statements will, instead, throw a compiler error.

What’s the difference between using Requires and using If-Then-Throw statements? An If-Then-Throw statement always throws the exception you indicate if validation fails. In this regard, it differs from Requires, but it’s similar to Requires<T>. A plain If-Then-Throw statement is also not discoverable by Contract tools (rewriter and static checker) unless you follow it with a call to EndContractBlock. When you use EndContractBlock, it must be the last Code Contract method you invoke in the method. No other Code Contracts call can ever follow it:

if (y == 0)
  throw new ArgumentException();
Contract.EndContractBlock();

In addition, Requires statements are automatically inherited. An If-Then-Throw statement is not inherited unless you also use EndContractBlock. In legacy mode, If-Then-Throw Contracts are not inherited. Instead you must manually do the Contract inheritance. The tools will try to warn if they do not detect that the preconditions are repeated in overrides and interface implementations.

Finally, note that ContractAbbreviators are not allowed to contain any If-Then-Throw statements, but you can use Contract validators for that. Abbreviators can only include regular Contract statements for argument validation.

Other Settings

In the Code Contracts property page, if you select the Perform Runtime Contract Checking option, you’ll enable some additional useful options.

If you turn on the Assert on Contract Failure option, any violations of a contract will result in an assert that describes the context of the failure. You’ll see a message box similar to what’s shown in Figure 2 and will be given a few options to choose from. You can, for example, try to attach a debugger again, abort the application or simply ignore the failure and proceed.

You might want to use this option for debug builds only because the information displayed is not likely to be meaningful to the average end user. The Code Contracts API offers a centralized exception handler that captures any violation, leaving it up to you to figure out what exactly went wrong. Information you receive distinguishes whether a precondition, a postcondition or invariant failed, but only uses the Boolean expression and possibly the configured error message to characterize the error. In other words, it’s a bit difficult for you to recover gracefully from the centralized exception handler:

Contract.ContractFailed += CentralizedErrorHandler;

Here’s some code that illustrates the handler:

static void CentralizedErrorHandler(
  Object sender, ContractFailedEventArgs e) {
  Console.WriteLine("{0}: {1}; {2}", e.
    FailureKind, e.Condition, e.Message);
  e.SetHandled();
}

If you want to throw specific exceptions at run time, then using Requires<TException> is the way to go. You might want to use Requires and the centralized handler if you intend to limit the use of Contracts to debug builds or if you don’t care what the actual type of the exception is. It’s often enough just to indicate that an error occurred. For instance, at the top level, many applications have a catch-all that catches every type of exception and figures out how to restart.

The Only Public Surface Contract option refers to where you would like to have Code Contracts enforced: every method or only public methods. If you check the option, then the rewriter ignores Code Contract statements on private and protected members and it only processes Contracts on public members.

Checking this option makes sense if you incorporate Code Contracts as part of your overall design and, as a result, use them everywhere. However, once the application is ready to ship, as a form of optimization you can turn off the extra burden of checking parameters on internal members because no external code will ever be invoking those members directly.

Whether limiting Code Contracts to the public surface of an assembly is a good idea also depends on how you’ve written the code. It’s a form of optimization if you can guarantee that any calls the public surface makes to lower levels are correct. If not, disabling contracts for internal methods can turn into the source of nasty bugs.

The Call-site Requires Checking option serves another optimization scenario. Suppose you’re writing a library to be used by modules in other assemblies. For performance reasons, you disable runtime checking of Contracts. However, as long as you also create a Contract reference assembly, you enable the caller to check the Contract for each method being called.

A Contract reference assembly may exist for every assembly that contains classes using Code Contracts. It contains the publicly visible interface of the parent assembly with Contract statements, but no other code. The creation of the assembly can be ordered and controlled from the Code Contracts property page.

Any code that intends to invoke your library may reference your Contract reference assembly and could automatically import your Contracts by simply turning on the Call-site Requires Checking option. When processing the caller code, the rewriter will import the Contract for every method being called on an external assembly that comes with a Contract reference assembly. In this case, the Contract is checked at the call-site—on the caller side—and remains an optional behavior that can be turned on and off for code you don’t control directly.

Wrapping Up

Code Contracts is an area of the .NET Framework that’s worth a lot more investigation. I’ve just scratched the surface of the configuration options here and haven’t even gone into the use of the static checker. Code Contracts help you design your apps more clearly and write cleaner code.

To learn more about Code Contracts, see the June 2009 CLR Inside Out column by Melitta Andersen (msdn.microsoft.com/magazine/ee236408) and the DevLabs Code Contracts site (msdn.microsoft.com/devlabs/dd491992). You’ll also find interesting background information about the development of Code Contracts at the Microsoft Research Code Contracts site (research.microsoft.com/projects/contracts).

---

Dino Esposito is the author of “Programming Microsoft ASP.NET MVC” (Microsoft Press, 2010) and coauthor of “Microsoft .NET: Architecting Applications for the Enterprise” (Microsoft Press, 2008). Based in Italy, Esposito is a frequent speaker at industry events worldwide. Follow him on Twitter at twitter.com/despos.

Thanks to the following technical expert for reviewing this article: Mike Barnett