Monthly Archives: April 2011

My Foray into Code Contracts

Download Sample Solution – Code Contracts from my site

To completely walk through the following sections, you will need the following:

  1. Visual Studio 2008 or Visual Studio 2010 (most of this will NOT work with Express editions)
  2. Download Code Contracts Premium Edition from
    1. Only if you have Visual Studio 2008 Team Edition, Visual Studio 2010 Premium or Ultimate
    2. Code Contracts Standard Edition doesn’t support static checker
  3. Download Code Contracts Editor Extensions from Visual Studio Extension Manager (optional)
  4. Download and install Visual Studio 2010 Pex – White Box Unit Testing for .NET from Visual Studio Extension Manager
  5. Download Sandcastle from CodePlex

Visual Studio has always helped me write better code and yet I still write plenty of bugs! Am I getting worse as Visual Studio gets better?! J

That’s why I no longer know how I’d write code without a unit test framework. I now write better code because I can test it in different ways in an automated fashion – as opposed to manually running through a UI trying to find every code path. I still have trouble coming up with all the various paths to test, but more on that later.

Search the solution for “// Step 1: “, but don’t expand the region before trying to answer the question it poses.

private static double ReadDoubleAttribute(XElement element, string attribute)
    // Step 1: 
    #region What is wrong with the following line of code?
    // no peeking!
    return Double.Parse(element.Attribute(attribute).Value);

Custom Parameter Validation

Most of the time, you will try to validate input parameters with if…then…throw code. This works fine, but it can require a lot of code and you have to remember to enter even the most basic null checks.

Search the solution for “// Step 2: ” for a typical examples of this.

private static int ReadIntegerAttribute(XElement element, string attribute)
    // Step 2: Example of traditional parameter validation - note that static checker accepts this
    if (element == null)
        throw new ArgumentNullException("element");
    if (String.IsNullOrEmpty(attribute))
        throw new ArgumentNullException("attribute");
    if (element.Attribute(attribute) == null)
        throw new ArgumentException("Attribute was not found.");

    return Int32.Parse(element.Attribute(attribute).Value);

Enabling Code Contracts

Open the project properties for IntelligenceDatabase.UI.Windows.

Click on the Code Contracts tab.

Set Assembly Mode to Standard Contract Requires to utilize contracts in your build. Under Contract Reference Assembly, select Build and enable Emit contracts into XML doc file.

Enable Perform Runtime Contract Checking and set it to Full. Lower levels ignore certain types of contract checks.

Enable Perform Static Contract Checking to utilize the static checker while writing code. Enable all of the following options:

  • Check in Background – static checker runs in background so as not to block the build
  • Show squiggles – underline contract violations in the code editor
  • Implicit Non-Null Obligations – check for possible null reference issues
  • Implicit Arithmetic Operations – check for possible math problems like divide by zero
  • Implicit Array Bounds Obligations – check for possible misuse of array indexes
  • Redundant Assumptions – check for assumptions that can be proven (will make more sense when we get to Contract.Assume)

Build the solution and check out the warnings and messages in the Error List.

Notice the static checker returns warnings for the ReadDoubleAttribute method (Step 1). It notices the possible call on a null reference, the attribute parameter could be a null or empty string, and the element parameter could be null.

It doesn’t return any warnings for the ReadIntegerAttribute method (Step 2). This is because the static checker sees these traditional parameter checks at the top of the method.


Search the solution for “// Step 3: “. The ReadStringAttribute method has many of the same problems as the ReadDoubleAttribute. Uncomment the next line to see a standard example of a Contract.Requires. This says that the element parameter cannot be null when it enters this method. The associated warning should be removed after rebuilding.

// Step 3: The static checker will flag element as a possible null reference exception
Contract.Requires<ArgumentNullException>(element != (XElement)null"element");

It is common to use the Contract.Requires<[exception type]>([boolean test], [message]); format to throw the specified exception with the message when the Boolean test fails. You can omit the [exception type] and/or [message] as desired.

Search the solution for “// Step 4: “. Uncomment the subsequent line that verifies the attribute parameter is not a null or empty string. The associated warning should be removed after rebuilding.

// Step 4: The static checker will flag attribute as a possibly null or empty string
Contract.Requires<ArgumentException>(!String.IsNullOrEmpty(attribute), "Attribute was not found");

Note that contracts can also be defined to iterate through collections. See Contract.ForAll or Contract.Exists for more information.

Assert & Assume

Search the solution for “// Step 5: “, uncomment the subsequent line, and rebuild.

// Step 5: The static checker will flag a null return from the Attribute method as a possible null reference exception
Contract.Requires<ArgumentException>(element.Attribute(attribute) != null);

Whoah! You probably got about a dozen more warnings, huh? The problem is that every caller of this method cannot prove the attribute will be found in the XML. If you mouse over the Attribute method, you will see a message stating that this method has no contracts. Re-comment the line under Step 5 and rebuild to revert to the single warning.

Contract.Assert can be used if you know something must be true at a certain point in a program and you want the static checker to verify it. Search the solution for “// Step 6: “, uncomment the subsequent line, and rebuild.

// Step 6: Find warning for 'element.Attribute(attribute).Value; uncomment the following line and rebuild - new warning!
Contract.Assert(element.Attribute(attribute) != null);

Still didn’t work? Using Contract.Assert doesn’t in and of itself prove the contract. The best fix would be to add an if-then-throw check to verify null was not returned by the Attribute method before calling the Value property. Re-comment the line under Step 6 and rebuild to revert to the previous warning.

Sometimes you want to tell the static checker that you know what the state of the program will be at a certain point, but it can’t prove it. Use Contract.Assume to do this. Search the solution for “// Step 7: ” and uncomment the subsequent line to remove the warning. This is a hack, but we’ll come back to Contract.Assert and Contract.Assume later.


Interfaces are the classic example of a contract in programming. Code contracts can be used to supplement an interface. We can’t define contracts within an interface because you can’t implement any of its members. Hmmm…

Search the solution for “// Step 8: “. See the attribute used on the interface to define the type where the code contracts will be defined.

// Step 8: Notice ContractClassAttribute used to designate contract implementation
/// <summary>
/// This interface represents all types of characters
/// </summary>

public interface ICharacter

Search the solution for “// Step 9: “. Note the attribute and the abstract class modifier that designate this as a contract class. While this feels a bit ugly to create another class, you can’t implement interface members so this is what you got. You might feel a bit better to put this derived class definition in the same file as the interface definition – or you may not. J

// Step 9: Notice ContractClassForAttribute to designate which class this contract implementation is for
/// <summary>
/// Defines the contracts for the ICharacter interface
/// </summary>

public abstract class ICharacterContract : ICharacter


/// <summary>
    /// Defines the contracts for getting and setting the value of the Essence attribute
    /// </summary>
    public double Essence


            Contract.Ensures(Contract.Result<double>() > 0);
            Contract.Ensures(Contract.Result<double>() <= 6);
throw new NotImplementedException();
            Contract.Requires((value > 0) && (value <= 6));
throw new NotImplementedException();

/// <summary>
    /// The object invariant method that ensures an instance of this object never violates any contracts defined here

    /// </summary>
    private void ObjectInvariant()
        Contract.Invariant(Essence > 0);
        Contract.Invariant(Essence <= 6);

All implementations of this interface will not only have to adhere to these contracts, but they can’t even define their own! This has caused me several headaches after I implement these interfaces, but maybe it’s just me.

We’ll revisit the Contract.Ensures and ObjectInvariant methods shortly.


Contract.Requires is also known as a precondition. It states that something must be true prior to entering this method. Wouldn’t it be great if we could also state that something is true when we leave a method? Search the solution for “// Step 10: ” Contract.Ensures is a postcondition that states this property will always return an integer greater than zero.

/// <summary>
/// Gets or sets the maximum number of condition boxes this critter can have
/// </summary>
public int MaximumConditionBoxes


        // Step 10: The value of this property must always be at least one
        Contract.Ensures(Contract.Result<int>() > 0);

        return _maximumConditionBoxes;

Like Contract.Requires, the Contract.Ensures method must appear at the top of a member where it essentially defines the signature of the member. Also, note the Contract.Result<T> method. This method can be used within postconditions to represent the return value of a method or property.

Object Invariants

In order to remain valid, some classes need to have certain conditions hold true the entire life of the object.

// Step 11: These contracts hold true throughout an object's lifecycle
/// <summary>
/// The object invariant method that ensures an instance of this object never violates any contracts defined here
/// </summary>

private void ObjectInvariant()

    Contract.Invariant(this._currentConditionBoxes > 0);
    Contract.Invariant(this._maximumConditionBoxes > 0);

Invariants are checked upon the exit of every public member. No other code can be present in an invariant method.

TIP: Commonly-used contract definitions can be consolidated into ContractAbbreviator methods for reuse.

Verify your contracts work as you expect them to. Open the GruntTest.cs file. Run the three tests for the CurrentConditionBoxes property and walkthrough the code for each one.

Contract Documentation

After ensuring you’ve built the application, navigate to C:\Projects\IntelligenceDatabase\Development\DEV1\IntelligenceDatabase\IntelligenceDatabase.Windows\IntelligenceDatabase.UI.Windows\bin\Debug and double-click the Documentation.xml file. You should see some XML comments for ensures and requires throughout the document. Use this XML file with your favorite documentation builder to include contract information.


Like Code Contracts, Pex is another technology brought to you by the fine folks at Microsoft Research. Pex is a white box testing tool and is therefore closely associated with code contracts. You can use it to help you add the right contracts to a method.

Search the solution for “// Step 12: “. Right-click the class name (CharacterCollection) and select Run Pex from the context menu. After Pex has completed running, you should see two test failures in the Pex Explorer window. Click one of the failed tests for the constructors to see the stack trace. CharacterCollection inherits from ObservableCollection<T>. Calling the base constructors with a null parameter will result in an ArgumentNullException.

Search the solution for “// Step 13: “, uncomment the subsequent line, and re-run Pex on the class from the Pex Exploration Results window. You should only have one test failure now.

/// <summary>
/// Instantiates a collection initialized by any enumerable set of characters
/// </summary>
/// <param name="collection">An enumerable set of characters</param>
public CharacterCollection(IEnumerable<ICharacter> collection)

    : base(collection)


    // Step 13: Uncomment to make Pex tests succeed

    Contract.Requires<ArgumentNullException>(collection != null);