.NET 4 Feature Focus: Code Contracts

Last year we started talking about Spec#, a language based on C# that supports design by contract. Design by contract builds on top of concepts like static typing, where certain actions cannot be performed unless it can be verified at compile time. Contracts usually take the form of pre- and post-conditions such as a parameter or return value never being null or only containing a certain range of values.

Rather than force developers to learn a whole new language such as Spec#, Microsoft is working on a language-agnostic library that can be leveraged by any .NET language. In some ways contracts look like assertions, but they are very different under the covers. Contracts are supported by a combination of static code analysis, which can be both inside and outside the compiler, as well as by testing frameworks. They are also executable, meaning they behave like assertions when running a debug build. Consider this first example:

string GetDescription(int x){
Contract.Requires(x>0);
Contract.Ensures(Contract.Result<string>() != null);

Looking at just the signature, developers only get the static type information "GetDescription requires an integer and returns a string". With the contracts, both developers and tools know "GetDescription requires a positive integer and returns a string that is never null".

In addition to explicit contracts, the contract checker can also support implicit contracts. One such example is division by zero. If a class includes a division of integers where the divisor is a variable, then all code paths must ensure that the variable is never zero or a warning is issued. If the variable in question is a property on a unsealed class, this would require checking in every subclass as well. There are also implicit contracts for dereferencing nulls and array indexes.

To make this easier, there is the concept of an ObjectInvariant method. This special method, which only contains contracts, is injected into the end of each method call to ensure the object's state remains consistent. It is important to note that this applies to all methods, including those in subclasses from other assemblies.

Another time saving device is easy access to old values. In this example the Ensures contract is used in conjunction with the OldValue syntax to make certain that the collection's count property is incremented.

Public Sub Add(value as Object) 
Contract.Ensure(Count = Contract.OldValue(Count) + 1) 

Even though the contract is written at the top of the method, it will automatically be moved to just before the Return statement by the compiler. As there is some overhead for storing the old value of Count, this sort of check will only occur in debug builds.

In order to support library developers, release builds include a reference assembly. For example, the Widgets.dll assembly would have the bulk of its contracts extracted and placed in the assembly Widgets.Contracts.dll. This allows client developers to use the faster release-style builds while still leveraging the contracts created by the library developers.

One of the more interesting features is that contracts do not just apply to concrete functions. Even interface and abstract methods with no other implementation detail can have contracts. This is done by creating a reference implementation of the interface whose sole purpose is to hold contracts. This reference implementation is linked back to the interface by attributes.

There are no restrictions on the contents of a contract. Since the same contracts are used for both static and runtime checking, a complex constraint that cannot be evaluated by one may still be checked by the other. Contracts can also be extracted by documentation generators.

For more information on Contracts in .NET 4, check out the first half of this PDC keynote.