What’s up with code contracts?

Code contracts are used as a tool that allows developers to put specific restrictions on what their code does.

For example, with the help of code contracts, specific pre-conditions can be set before a method is executed, that must be met before the method will start working. Or there could be post-conditions for the same method that define the expected values and if those are not the ones the program was waiting for, then the method fails.

A look overboard – conditional constants

Conditionals are a nice tool when you want to customize the way the application works depending on the passed launch parameters. The developer can decorate specific methods with ConditionalAttribute (System.Diagnostics should be declared in order to use this attribute) and those will only be executed when there are suitable constants defined via the /define parameter or directly in code via #define. For example, there is a sample console application that has a PrintThis method:

using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.Diagnostics;

namespace ConsoleApplication
{
    class Program
    {
        static void Main(string[] args)
        {
            PrintThis("Hello!");
        }

        [ConditionalAttribute("PRINT_THIS")]
        static void PrintThis(string text)
        {
            Console.WriteLine(text);
        }
    }
}

If you run the application, no message will be displayed:

What makes this method different from any other method is it’s attribute, that specifies that PrintThis will only be executed when the PRINT_THIS parameter will be passed as a conditional compilation symbol. And this can be done in several ways.

The first one (and probably the easiest one) is to set the constant before the namespace declarations. To do this, you can use #define PRINT_THIS.

The second way to do this is by specifying the conditional compilation symbol in the application properties dialog:

You can also use command-line arguments (via /define:CONSTANT_NAME). Either way, when you launch the application now, you can see that the string is being displayed:

And this is how conditional constants work. Later on you will see why I made an introduction to these first.

Code contracts – getting started

First of all you need to declare the System.Diagnostics.Contracts namespace. This will let you work with the Contract object, which is basically the core element for code contracts.

But this is not it just yet. Before going into testing code that has code contracts implemented, you will need one more tool –the binary rewriter, that will allow exceptions to be thrown at runtime in case some contract condition is not satisfied.

You can download the tools here – available at no cost, but requiring a commercial edition of Visual Studio 2010 installed.

If you will not use the rewriter, by default the contracts won’t be even touched so you will see no effect whatsoever on the program. However, code contracts are also based on conditional constants – for example the methods present in the Contract object are executed only when there is a CONTRACTS_FULL symbol defined – so I thought – well, I can always declare the symbol manually and therefore force the contracts to be linked to their methods. Not so fast:

A rewriter is still needed for contracts to work at runtime. So once you download and install the tools, you should be all set.

Pre-conditions

Code contracts offer the possibility to check for pre-conditions before executing a method. For example, for the same PrintThis method shown above, I would like to execute it only if the passed string is equal to “Hello!” With this in mind, inside the method I am declaring a pre-condition:

static void PrintThis(string text)
{
    Contract.Requires(text == "Hello!");
    Console.WriteLine(text);
}

Pass a random string to the method (not equal to the pre-condition) and see the code… fail. You will get the same message you got before regarding the use of a rewriter. Although you installed the tools, you did not configure the contracts for the specific project.

NOTE: At this point you will not need the CONTRACTS_FULL symbol, so feel free to remove the #define from your code file.

If you open the Project Properties dialog, you will see that there is a new tab added – Code Contracts:

That’s the place where you can configure the contract linking process. For now, enable full runtime contract checking (since I will show samples using various conditions):

The Requires method checks against a Boolean value, so if the check fails, you get a ContractException:

In case you want to throw your own exception as well as use a custom exception message, you can use another type of the same Requires method:

Contract.Requires<NotImplementedException>(text == "Hello!","Failed!");

Here, if the contract fails, I will get a NotImplementedException with the “Failed!” message. But before using this, you need to switch to Standard Contract Requires:

Note that once a contract pre-condition is defined, no statements can go before it (unless those are also a part of a contract, but then it is needed to be separate them by Contract.EndContractBlock()).

Post-conditions

Unlike pre-conditions, post-conditions are used to verify the state of the method after it was executed. To do this, I can use the Ensures method (also in the Contract class). Here is the modified version of the PrintThis method that is using a post-condition:

static string PrintThis(string text)
{    
    Contract.Ensures(Contract.Result<string>() == "HELLO WORLD");
    return text.ToUpper() + " WORLD";
}

Test it on a string that is different from “hello” and you will see that the code breaks – the contract is not satisfied. Contract.Result<T> represents the returned value for the contract, so you don’t have to worry about passing it explicitly to verify the output.

In case you want to call a contract once an exception is thrown, you can rely on EnsuresOnThrow<T>, where T is the type of exception to be thrown:

Contract.EnsuresOnThrow<Exception>(!string.IsNullOrEmpty(text), "Failed!");

However, be very careful with the type of the exception – if the exception thrown by the method will not be the one specified in the contract, it will not be called and this may eventually lead to incorrectly functioning code.

What if it fails?

When a contract fails, a ContractException is thrown notifying the developer that the contract was not satisfied and that the data is invalid. A failed contract is handled via the ContractFailed event handler:

Contract.ContractFailed += new EventHandler<ContractFailedEventArgs>(Contract_ContractFailed);

This means that you can customize the process in case of a contract failure the same way you do for any other event handler:

static void Contract_ContractFailed(object sender, ContractFailedEventArgs e)
{
    Debug.Print("The contract failed!");
}

Note, that it will still throw a ContractException, even if the ContractFailed event handle is set. Its purpose is to give you a hand when it comes to determining at runtime whether a contract is satisfied or not.

If you want to know what type the condition had (post-condition or pre-condition), you can call the passed ContractFailedEventArgs instance and access its FailureKind property. In case you need to know the condition, it is exposed by the same instance, but by the Condition property.

Conclusion

As you can see, code contracts can be a useful tool. Making sure that a method gets and sets correct values is a task that often requires some additional work. Code contracts in this case help you ensure the code works exactly the way it should and therefore make the application less prone to programming mistakes.