August 2009
Volume 24 Number 08
CLR Inside Out - Code Contracts
By Melitta Andersen | August 2009
This column is based on a prerelease version of the Microsoft .NET Framework 4. Details are subject to change.
Contents
Parts of the Code Contracts System
The Code Contract Library
Preconditions
Postconditions
Object Invariants
Other Contracts
Debugging with Code Contracts
Where to Get More Information
Often there are certain facts about code that exist only in the developer's head or, if you're lucky, in the code comments. For example, method Foo assumes that the input parameter is always positive and fails to do anything useful on negative numbers, so you had better make sure you're calling it with a positive number. Or class Bar guarantees that property Baz is always non-null, so you don't have to bother checking it. If you violate one of these conditions, it can lead to difficult-to-find bugs. In general, the later a bug is found, the more difficult it is to fix. Wouldn't it be great if there were a way to encode and check this kind of assumption to make it easier to catch bugs, or even help prevent you from writing them in the first place?
This is where programming with contracts comes in. The practice was first introduced by Bertrand Meyer with the Eiffel programming language. The basic idea is that classes and methods should explicitly state what they require and what they guarantee if those requirements are met, i.e., their contracts. Ideally, they are decided upon at design time, and not tacked on after development has already happened. These contracts are not only human-readable, but they can also be picked up by tooling that can perform runtime checking or static verification, or perhaps include them in generated documentation.
For those familiar with Debug.Assert, you may be thinking this is a solved problem. But Debug.Assert only allows you to express that a particular condition should be true at a particular point in the code. Code contracts allow you to declare once that a particular condition should hold any time certain events occur, such as every exit point from a method. They can also express invariants that should be true class-wide, or requirements and guarantees that should exist even for subclasses.
The Common Language Runtime (CLR) team is introducing a library to allow programming with contracts in the Microsoft .NET Framework 4. Adding them as a library allows all .NET languages to take advantage of contracts. This is different from Eiffel or Spec#, a language from Microsoft Research (research.microsoft.com/en-us/projects/specsharp/), where the contracts are baked into the language.
This article will share some of the best practices that the Base Class Libraries (BCL) team devised as it added the code contract libraries and started to take advantage of them in its own code. This article is based on a prerelease version of code contracts that is more recent than the beta 1 version, so there may be some details that are different from the released version. But the general principles should remain the same.
Parts of the Code Contracts System
There are four basic parts that are involved in using code contracts in the .NET Framework 4. The first part is the contract library. Contracts are encoded using static method calls defined in the Contract class in the System.Diagnostics.Contracts namespace in mscorlib.dll. Contracts are declarative, and these static calls at the beginning of your methods can be thought of as part of the method signature. They are methods, and not attributes, because attributes are very limited in what they can express, but the concepts are similar.
The second part is the binary rewriter, ccrewrite.exe. This tool modifies the Microsoft Intermediate Language (MSIL) instructions of an assembly to place the contract checks where they belong. With the library, you declare your contracts at the beginning of the method. Ccrewrite.exe will place checks for the method guarantees at all return points from the method and will inherit contracts from other locations, such as base classes or interfaces. This is the tool that enables runtime checking of contracts to help you debug your code. Without it, contracts are simply documentation and shouldn't be compiled into your binary.
The third part is the static checker, cccheck.exe, that examines code without executing it and tries to prove that all of the contracts are satisfied. This tool is used only for advanced scenarios where the programmer is willing to go through the effort required to track down unproven contracts and add extra information as needed. Attributes exist that let you specify which assemblies, types, or members should be checked. It is generally a good plan to start small and then expand the scope for your static analysis.
Running the rewriter and adding many extra checks to your assemblies is beneficial to help you catch errors and write quality code. But those checks can slow down your code, and you don't always want to include them in your shipping assemblies. However, if you are developing APIs that others might write code against, it would be useful for them to have access to the contracts for your code. To that end is the fourth part, the tool ccrefgen.exe, which will create separate contract reference assemblies that contain only the contracts. The rewriter and static checker will then make use of any contract assemblies when they are doing their instrumentation and analysis.
To get more information about all of these tools or to get the latest releases, please check the Code Contracts site on DevLabs: msdn.microsoft.com/en-us/devlabs/dd491992.aspx.
The Code Contract Library
There are three basic types of code contracts: preconditions, postconditions, and object invariants. Preconditions express what program state is required for the method to run successfully. Postconditions tell you what you can rely upon at the completion of the method. Object invariants are guarantees about conditions that will always be true for an object. They can be also thought of as postconditions that apply to every (public) method. Each of these three types has several flavors, and there are a few other types of contracts that we will eventually get into in some detail. If you want all of the nitty-gritty details about the library, please look in the documentation.
There are a few things that are common to all types of code contracts. First, since code contracts are primarily to help find bugs in code, they are conditionally compiled upon the symbol CONTRACTS_FULL. This way, the developer can choose whether to include the checks as needed. On the BCL team, most contracts are included in debug builds to provide more information for finding bugs, but are not included in retail builds. Second, all conditions that are checked by contracts must be side-effect free. Third, contracts are inherited. This is because you often have an API that expects type T, but might receive a subclass of T instead. The programmer expects T's guarantees to hold, and contract inheritance ensures this.
Preconditions
There are three basic forms of preconditions, two of which take the form of different Requires methods on the Contract class. Both of these also have overloads that allow you to include a message to display if the contract is violated. Here is an example of using Requires statements to encode preconditions:
public Boolean TryAddItemToBill(Item item) { Contract.Requires<NullReferenceException>(item != null); Contract.Requires(item.Price >= 0);
The Requires method is simply a way to encode that a particular condition must be true upon entry to the method. It can only use data that is at least as visible as the method itself, so that callers might actually be able to satisfy the condition. The other form, Requires<TException>, makes that same statement, but further guarantees that if the condition is not met, an exception of type TException should be thrown. It is also unique in that it is always compiled, so use of this method entails a hard dependency on the tools. You should decide if you want that before using this method.
The last form of precondition is something developers have been using since the beginning of the .NET Framework. It is the if-then-throw form used for parameter validation. For example:
public Boolean ExampleMethod(String parameter) { if (parameter == null) throw new ArgumentNullException("parameter must be non-null"); }
The benefit of this type of precondition is that it is always there to perform the runtime check. But there are several things that the code contract system provides that are not present with this form of validation: these exceptions can be swallowed by catch statements; they aren't inherited; and it is difficult for tools to recognize them. For that reason, there exists the Contract.EndContractBlock method. This method is a no-op at runtime, but indicates to the tools that all preceding if-then-throw statements ought to be treated as contracts. So, to let the tools know about these contracts, we could modify the above example as follows:
public Boolean ExampleMethod(String parameter) { if (parameter == null) throw new ArgumentNullException("parameter must be non-null"); // tells tools the if-check is a contract Contract.EndContractBlock();
Note that if-then-throw statements may appear in many places in your code, such as for validating user input, but the only place one counts as a contract is when it is at the beginning of your method and is followed by a call to EndContractBlock or one of the Requires or Ensures methods.
There are three different ways to encode preconditions, but which one should you use? That might vary from class to class or assembly to assembly, but there are some general guidelines you should follow. If you don't want to do any argument validation in your release code, use Requires. That way you enable contract checking only for your debug builds.
If you do want argument validation in your released code, there are several things to consider. One factor is whether you are writing brand new code or updating existing code. In the BCL, we use the if-then-throw contracts to match our existing patterns. This does mean that we need to do any inheritance manually, since we do not run the tools on our final builds. If you are writing new code, you can decide whether you want to use the old form or switch to the new form and get the other benefits of contracts. Part of that decision should be determining whether you are willing to take a dependency on the binary rewriter as part of your build process. The CLR team chose not to, as the tool is currently under active development. So, we use the if-then-throw form for anything we want to make sure is in the retail build, but we can use the Requires form for extra checks to help with debugging.
Postconditions
There are two basic types of postconditions: guarantees about normal returns and guarantees about exceptional returns. For this, there are two different methods on the Contract class. Again, each has an overload that will allow the developer to pass in a message for when the contract is violated. To continue with the example from the preconditions, here are some postconditions on that same method:
public Boolean TryAddItemToBill(Item item) { Contract.Ensures(TotalCost >= Contract.OldValue(TotalCost)); Contract.Ensures(ItemsOnBill.Contains(item) || (Contract.Result<Boolean>() == false)); Contract.EnsuresOnThrow<IOException>(TotalCost == Contract.OldValue(TotalCost))
The Ensures method simply makes a statement about a condition that is guaranteed to be true at normal return from a method. In general, these methods are not intended to be included in your retail builds, but are only for debugging purposes. Their use is encouraged wherever they make sense. EnsuresOnThrow<TException> makes a guarantee for the case where a particular exception is thrown. The ability to make statements about exceptional conditions is another benefit over a simple Debug.Assert. Note that this should only be used for exceptions that you expect to throw from your method and should be as specific as possible. Using the type Exception for TException is not recommended, as then you are making guarantees about program state after events you do not control, such as an OutOfMemoryException or StackOverflowException.
You may have noticed some extra Contract methods in that example. In order to express more useful postconditions, it helps to have a way to express information about values at various points in the method. For example, say you have a method that ensures that the value of the instance at the end of the method is the same as the value when the method was called, and you want to be able to check that guarantee with contracts. The Contract class provides several methods that can only be used in postconditions to help out with that:
public static T Result<T>(); public static T OldValue<T>(T value); public static T ValueAtReturn<T>(out T value);
The Result<T> method is used to represent the return value of the method. OldValue<T> is used to represent the value of a variable at the beginning of the method. Each Ensures method is evaluated at any exit from a method, so all of the variables used refer to the value at the end of the method and no special syntax is needed. However, the Ensures methods are declared at the beginning of the method. So out parameters would not have been assigned to yet. Most compilers will complain about this, so the ValueAtReturn<T> method exists to allow you to use out parameters in postcondition contracts.
So if you wanted to implement the aforementioned example, you could write the following:
public class ExampleClass { public Int32 myValue; public Int32 Sum(Int32 value) { Contract.Ensures(Contract.OldValue(this.myValue) == this.myValue); myValue += value; //this violates the contact and will be caught return myValue; } }
Notice the error in the method above. It claims that myValue will be the same at the end of the method as it was at the beginning, but a line in the code violates that. When you enable contract checking, this bug will be detected and the developer can fix it.
One thing to keep in mind when writing postconditions is that they can be very difficult to get correct after the fact. We added some postconditions to the BCL that we thought were fairly straight-forward and obvious. But when we tested them, we found several of them that were violated in subclasses or in corner cases that we hadn't thought about. And we could not break the existing code to follow the new, cleaner postconditions, so we had to modify or remove our annotations. It helps to decide on the guarantees you want to make before you implement the class, so that you can catch any violations and fix them while you are writing them.
Object Invariants
The third major type of code contract is the object invariant. These are object-wide contracts about a condition that is guaranteed to always hold. They can be thought of as postconditions on every single public member of the object. Object invariants are encoded with the Invariant method on the Contract class:
public static void Invariant(bool condition); public static void Invariant(bool condition, String userMessage);
They are declared in a single method on the class that contains only calls to Invariant, and it must be marked with the ContractInvariantMethod attribute. It is common practice to name that method "ObjectInvariant" and to make it protected so that users cannot accidentally call this method. For example, an object invariant for the same object that contained the TryAddItemToBill method might be the following:
[ContractInvariantMethod] protected void ObjectInvariant() { Contract.Invariant(TotalCost >= 0); }
Again, it is useful to decide upon the object invariants before implementing the class. That way you can try to avoid violating them, and thus avoid writing bugs in the first place.
Other Contracts
The remaining contracts are very similar to Debug.Assert in that they make a guarantee only about a particular point in the code. In fact, if you are using code contracts, the following two methods can be used in place of Debug.Assert:
public static void Assert(bool condition); public static void Assert(bool condition, String userMessage); public static void Assume(bool condition); public static void Assume(bool condition, String userMessage);
These methods are conditionally compiled on both the CONTRACTS_FULL and DEBUG symbols, so that they can be used anywhere Debug.Assert would be. They are useful mainly for implementation details, such as placing requirements on internal data. At runtime, these two methods have the same behavior. The difference comes during static analysis. The static checker will attempt to prove any Assert, but it will treat the Assume statements as definitely true and add them to its collection of facts.
Debugging with Code Contracts
After you have taken the time to add contracts to your code, how can you take advantage of them to find bugs? One scenario is to run the static analysis tool and investigate any contracts it cannot prove. The other is to enable runtime checking. To get the most out of runtime checking, it helps to know what happens when a contract is violated or evaluates to false. There are two stages for this: notification and reaction.
When a failure is detected, the contract raises an event with the following EventArgs:
public sealed class ContractFailedEventArgs : EventArgs { public String Message { get; } public String Condition { get; } public ContractFailureKind FailureKind { get; } public Exception OriginalException { get; } public Boolean Handled { get; } public Boolean Unwind { get; } public void SetHandled(); public void SetUnwind(); public ContractFailedEventArgs(ContractFailureKind failureKind, String message, String condition, Exception originalException); }
Remember that this is still a prerelease version of the class, so things could fluctuate a bit before the final release.
There is no default handler for this event, so the recommended practice is to register one with your desired behavior, if you want behavior other than the default. You might treat this as simply a logging mechanism, and record the information according to your general practices. You can also choose to handle the failure with anything from tearing down the process to ignoring it and continuing. If you choose to do the latter, you should call SetHandled so that the next step of the failure will not take place. You might also just want to break into the debugger. When running the handlers, all exceptions are swallowed. But if you really want to unwind the stack, you can call SetUnwind. Then, after all of the handlers have been called, an exception will be thrown.
When adding contracts to the BCL, we quickly realized that registering a handler should be one of the first things you do in your code, either in your main method or as you start an AppDomain. Object invariants are checked after any constructor, so you might end up with contract failures before you are ready to handle them if you do not register your handler right away.
If no handler sets Handled or Unwind, the default behavior is an assertion. The exception to that is if the application is hosted, and then escalation policy is triggered so that the host can decide upon appropriate behavior. Skipping the handler, and letting the assertion happen, may be the most reasonable thing to do as you are developing. The dialog gives you the option to break into the debugger and find your problem, so you can fix it. Recall that contract violations are never an expected outcome, so they should always be fixed.
However, if you are testing code using a testing framework, assertions are likely not what you want. In that case, you want to register a handler that will report contract failures as test failures in your framework. Here is one example of how to do this with Visual Studio's unit test framework:
[AssemblyInitialize] public static void AssemblyInitialize(TestContext testContext) { Contract.ContractFailed += (sender, eventArgs) => { eventArgs.SetHandled(); eventArgs.SetUnwind(); // cause code to abort after event Assert.Fail(eventArgs.Message); // report as test failure }; }
Where to Get More Information
This article is mostly an overview of code contracts, as well as coverage of some best practices the BCL team developed as it started using contracts. To get more details on the class and find out what more you can do with code contracts, you should check out the MSDN documentation. As of the writing of this article, the documentation for code contracts in the first beta release of the Microsoft .NET Framework 4is available. There are also recordings of two talks from the 2008 Microsoft Professional Developers Conference that give some examples and demos of code contracts, specifically on some tools from Microsoft Research, and on new features in the CLR.
To get the tools and more information about their use, check out the Code Contracts site on DevLabs. The site contains a forum, documentation, an FAQ, and downloads for the tools.
Post your questions and comments on the CLR Team Blog at https://blogs.msdn.com/clrteam/archive/tags/CLR+Inside+Out/default.aspx.
Melitta Andersen is a Program Manager on the Base Class Libraries team of the CLR. She mainly works on base types, numerics, collections, globalization, and code contracts.