Nbsp;   Code Contracts

Code contracts provide a way for you to declaratively document design decisions that you’ve made about your code within the code itself. The contracts take the form of the following:

■ PreconditionsTypically used to validate arguments

■ PostconditionsUsed to validate state when a method terminates either due to a normal return or due to throwing an exception

■ Object InvariantsUsed to ensure an object’s fields remain in a good state through an ob- ject’s entire lifetime

Code contracts facilitate code usage, understanding, evolution, testing, documentation, and early error detection.10 You can think of preconditions, postconditions, and object invariants as parts of a method’s signature. As such, you can loosen a contract with a new version of your code, but you can- not make a contract stricter with a new version without breaking backward compatibility.

At the heart of the code contracts is the static System.Diagnostics.Contracts.Contract class.

public static class Contract {

// Precondition methods: [Conditional("CONTRACTS_FULL")] public static void Requires(Boolean condition);

public static void EndContractBlock();

// Preconditions: Always

public static void Requires<TException>(Boolean condition) where TException : Exception;

// Postcondition methods: [Conditional("CONTRACTS_FULL")] public static void Ensures(Boolean condition);

public static void EnsuresOnThrow<TException>(Boolean condition) where TException : Exception;

// Special Postcondition methods: Always public static T Result<T>();

public static T OldValue<T>(T value);

public static T ValueAtReturn<T>(out T value);

// Object Invariant methods: [Conditional("CONTRACTS_FULL")] public static void Invariant(Boolean condition);

// Quantifier methods: Always

public static Boolean Exists<T>(IEnumerable<T> collection, Predicate<T> predicate); public static Boolean Exists(Int32 fromInclusive, Int32 toExclusive,

Predicate<Int32> predicate);

public static Boolean ForAll<T>(IEnumerable<T> collection, Predicate<T> predicate); public static Boolean ForAll(Int32 fromInclusive, Int32 toExclusive,

Predicate<Int32> predicate);

// Helper methods: [Conditional("CONTRACTS_FULL")] or [Conditional("DEBUG")] public static void Assert(Boolean condition);

10 To help with automated testing, see the Pex tool created by Microsoft Research: http://research.microsoft.com

/en-us/projects/pex/.

public static void Assume(Boolean condition);

// Infrastructure event: usually your code will not use this event

public static event EventHandler<ContractFailedEventArgs> ContractFailed;

}

As previously indicated, many of these static methods have the [Conditional("CONTRACTS_ FULL")] attribute applied to them. Some of the helper methods also have the [Conditional­ ("DEBUG")] attribute applied to them. This means that the compiler will ignore any code you write that calls these methods unless the appropriate symbol is defined when compiling your code. Any methods marked with “Always” mean that the compiler always emits code to call the method. Also, the Requires, Requires<TException>, Ensures, EnsuresOnThrow, Invariant, Assert, and Assume methods have an additional overload (not shown) that takes a String message argument so you can explicitly specify a string message that should appear when the contract is violated.

By default, contracts merely serve as documentation because you would not define the CONTRACTS_FULL symbol when you build your project. In order to get some additional value out of using contracts, you must download additional tools and a Visual Studio property pane from http://msdn.microsoft.com/en-us/devlabs/dd491992.aspx. The reason why all the code contract tools are not included with Visual Studio is because this technology is being improved rapidly. The Microsoft DevLabs website can offer new versions and improvements more quickly than Visual Studio itself. After downloading and installing the additional tools, you will see your projects have a new property pane available to them, as shown in Figure 20-9.

FIGURE 20-9The Code Contracts pane for a Visual Studio project.

To turn on code contract features, select the Perform Runtime Contract Checking check box and select Full from the combo box next to it. This defines the CONTRACTS_FULL symbol when you build your project and invokes the appropriate tools (described shortly) after building your project. Now, at run time, when a contract is violated, Contract’s ContractFailed event is raised. Usually, develop- ers do not register any methods with this event, but if you do, then any methods you register will receive a ContractFailedEventArgs object that looks like this.

public sealed class ContractFailedEventArgs : EventArgs {

public ContractFailedEventArgs(ContractFailureKind failureKind, String message, String condition, Exception originalException);

public ContractFailureKind FailureKind { get; } public String Message { get; }

public String Condition { get; }

public Exception OriginalException { get; }

public Boolean Handled { get; } // true if any handler called SetHandled

public void SetHandled(); // Call to ignore the violation; sets Handled to true

public Boolean Unwind { get; } // true if any handler called SetUnwind or threw public void SetUnwind(); // Call to force ContractException; set Unwind to true

}

Multiple event handler methods can be registered with this event. Each method can process the contract violation any way it chooses. For example, a handler can log the violation, ignore the viola- tion (by calling SetHandled), or terminate the process. If any method calls SetHandled, then the violation will be considered handled and, after all the handler methods return, the application code is allowed to continue running unless any handler calls SetUnwind. If a handler calls SetUnwind, then, after all the handler methods have completed running, a System.Diagnostics.Contracts. ContractException is thrown. Note that this type is internal to MSCorLib.dll and therefore you cannot write a catch block to catch it explicitly. Also note that if any handler method throws an unhandled exception, then the remaining handler methods are invoked and then a Contract­ Exception is thrown.

If there are no event handlers or if none of them call SetHandled, SetUnwind, or throw an unhandled exception, then default processing of the contract violation happens next. If the CLR is being hosted, then the host is notified that a contract failed. If the CLR is running an application on a non-interactive window station (which would be the case for a Windows service application), then Environment.FailFast is called to instantly terminate the process. If you compile with the Assert

On Contract Failure check box selected, then an assert dialog box will appear allowing you to connect a debugger to your application. If this option is not selected, then a ContractException is thrown.

Let’s look at a sample class that is using code contracts.

public sealed class Item { /* ... */ } public sealed class ShoppingCart {

private List<Item> m_cart = new List<Item>(); private Decimal m_totalCost = 0;

public ShoppingCart() {

}

public void AddItem(Item item) { AddItemHelper(m_cart, item, ref m_totalCost);

}

private static void AddItemHelper(List<Item> m_cart, Item newItem, ref Decimal totalCost) {

// Preconditions: Contract.Requires(newItem != null);

Contract.Requires(Contract.ForAll(m_cart, s => s != newItem));

// Postconditions:

Contract.Ensures(Contract.Exists(m_cart, s => s == newItem)); Contract.Ensures(totalCost >= Contract.OldValue(totalCost)); Contract.EnsuresOnThrow<IOException>(totalCost == Contract.OldValue(totalCost));

// Do some stuff (which could throw an IOException)... m_cart.Add(newItem);

totalCost += 1.00M;

}

// Object invariant [ContractInvariantMethod] private void ObjectInvariant() {

Contract.Invariant(m_totalCost >= 0);

}

}

The AddItemHelper method defines a bunch of code contracts. The preconditions indicate that newItem must not be null and that the item being added to the cart is not already in the cart. The postconditions indicate that the new item must be in the cart and that the total cost must be at least as much as it was before the item was added to the cart. The postconditions also indicate that if Add­ ItemHelper were to throw an IOException for some reason, then totalCost is unchanged from what it was when the method started to execute. The ObjectInvariant method is just a private method that, when called, makes sure that the object’s m_totalCost field never contains a negative value.

So now you see how to declare contracts. Let’s now talk about how they function at run time. You get to declare all your precondition and postcondition contracts at the top of your methods where they are easy to find. Of course, the precondition contracts will validate their tests when the method is invoked. However, we don’t want the postcondition contracts to validate their tests until the method returns. In order to get the desired behavior, the assembly produced by the C# compiler must be processed by the Code Contract Rewriter tool (CCRewrite.exe, found in C:\Program Files (x86)\Microsoft\Contracts\Bin), which produces a modified version of the assembly. After you select

the Perform Runtime Contract Checking check box for your project, Visual Studio will invoke this tool for you automatically whenever you build the project. This tool analyzes the IL in all your methods and it rewrites the IL so that any postcondition contracts are executed at the end of each method. If your method has multiple return points inside it, then the CCRewrite.exe tool modifies the method’s IL code so that all return points execute the postcondition code prior to the method returning.

The CCRewrite.exe tool looks in the type for any method marked with the [ContractInvariant­ Method] attribute. The method can have any name but, by convention, people usually name the method ObjectInvariant and mark the method as private (as I’ve just done). The method must accept no arguments and have a void return type. When the CCRewrite.exe tool sees a method marked with this attribute, it inserts IL code at the end of every public instance method to call

the ObjectInvariant method. This way, the object’s state is checked as each method returns to ensure that no method has violated the contract. Note that the CCRewrite.exe tool does not modify a Finalize method or an IDisposable’s Dispose method to call the ObjectInvariant method

because it is OK for an object’s state to be altered if it is considered to be destroyed or disposed. Also note that a single type can define multiple methods with the [ContractInvariantMethod] at- tribute; this is useful when working with partial types. The CCRewrite.exe tool will modify the IL to call all of these methods (in an undefined order) at the end of each public method.

The Assert and Assume methods are unlike the other methods. First, you should not consider them to be part of the method’s signature, and you do not have to put them at the beginning of a method. At run time, these two methods perform identically: they just verify that the condition

passed to them is true and throw an exception if it is not. However, there is another tool, the Code Contract Checker (CCCheck.exe), which analyzes the IL produced by the C# compiler in an attempt to statically verify that no code in the method violates a contract. This tool will attempt to prove that any condition passed to Assert is true, but it will just assume that any condition passed to Assume

is true and the tool will add the expression to its body of facts known to be true. Usually, you will use Assert and then change an Assert to an Assume if the CCCheck.exe tool can’t statically prove that the expression is true.

Let’s walk through an example. Assume that I have the following type definition.

internal sealed class SomeType {

private static String s_name = "Jeffrey";

public static void ShowFirstLetter() {

Console.WriteLine(s_name[0]); // warning: requires unproven: index < this.Length

}

}

When I build this code with the Perform Static Contract Checking function turned on, the CCCheck.exe tool produces the warning shown as a comment in the preceding code. This warn- ing is notifying me that querying the first letter of s_name may fail and throw an exception because it is unproven that s_name always refers to a string consisting of at least one character.

Therefore, what we’d like to do is add an assertion to the ShowFirstLetter method.

public static void ShowFirstLetter() {

Contract.Assert(s_name.Length >= 1); // warning: assert unproven Console.WriteLine(s_name[0]);

}

Unfortunately, when the CCCheck.exe tool analyzes this code, it is still unable to validate that s_name always refers to a string containing at least one letter, so the tool produces a similar warning. Sometimes the tool is unable to validate assertions due to limitations in the tool; future versions of the tool will be able to perform a more complete analysis.

To override shortcomings in the tool or to claim that something is true that the tool would never be able to prove, we can change Assert to Assume. If we know for a fact that no other code will modify s_name, then we can change ShowFirstLetter to this.

public static void ShowFirstLetter() { Contract.Assume(s_name.Length >= 1); // No warning at all now! Console.WriteLine(s_name[0]);

}

With this version of the code, the CCCheck.exe tool just takes our word for it and concludes that s_name always refers to a string containing at least one letter. This version of the ShowFirstLetter method passes the code contract static checker without any warnings at all.

Now, let’s talk about the Code Contract Reference Assembly Generator tool (CCRefGen.exe).

Running the CCRewrite.exe tool to enable contract checking helps you find bugs more quickly, but all the code emitted during contract checking makes your assembly bigger and hurts its run-time performance. To improve this situation, you use the CCRefGen.exe tool to create a separate contract reference assembly. Visual Studio invokes this tool for you automatically if you set the Contract Refer- ence Assembly combo box to Build. Contract assemblies are usually named AssemName.Contracts.dll (for example, MSCorLib.Contracts.dll), and these assemblies contain only metadata and the IL that describes the contracts—nothing else. You can identify a contract reference assembly because it will

have the System.Diagnostics.Contracts.ContractReferenceAssemblyAttribute applied to the assembly’s assembly definition metadata table. The CCRewrite.exe tool and the CCCheck.exe tool can use contract reference assemblies as input when these tools are performing their instrumentation and analysis.

The last tool, the Code Contract Document Generator tool (CCDocGen.exe), adds contract in- formation to the XML documentation files already produced by the C# compiler when you use the compiler’s /doc:file switch. This XML file, enhanced by the CCDocGen.exe tool, can be processed by Microsoft’s Sandcastle tool to produce MSDN-style documentation that will now include contract information.

C HA P T E R 2 1

Date: 2016-03-03; view: 656