No Interface Without Contract? – Part 5: Using Microsoft Code Contracts

Microsoft Code Contracts? Get started using them!

In the previous part we had a first look on Microsoft Code Contracts. This part will help us getting started using them.

Download and Installation

To use MS Code Contracts you need at least the Standard Edition of Visual Studio 2008 (VS 2010 is also supported).

You can download the installer from the project home page or from the other one. Depending on how you will use (commercial or non-commercial) you have to Screenshot of the Code Contracts pane in VSchoose between three editions:

After some clicks “on the “Next” buttons, the installation is complete.

Visual Studio Integration

When starting VS now and opening / creating a project, the project properties should have a new pane “Code Contracts” now; see the screenshot on the right. This pane allows you to configure the rewriter we will talk about later.

For the beginning, it should be enough to simply check “Perform Runtime Contract Checking” and leave everything else as it is.

One thing you also have to do manually: Add a reference to “Microsoft.Contracts Library” which is registered in the GAC.

The rewriter

By checking the “Perform Runtime Contract Checking” we activated the rewriter for this project. After the C#-Compiler has compiled our project, a build task will be started launching the rewriter. This rewriter now rewrites all calls to members of the static class Contract. Some rewriting is quite simple, some is more complicated.

Rewriting the assembly allows specifying the postconditions before the real code. In order to support debugging, the PDBs are also rewritten.

Working with Code Contracts

Preconditions

Preconditions are specified using Contract.Requires.

A method with a very simple precondition would be:

public void Bar(string parameter)
{
    Contract.Requires(parameter != null);
}

The plain Contract.Requires (without generic arguments) is intended to verify internal precondition. If it fails, a ContractException (internal so you can not explicitly catch it) will be thrown. If you want to, you can also specify a message (Note: The next version of Code Contracts will support static properties / fields as source for the message). Otherwise a default message including the condition (“parameter != null”) in this case will be used.

On public classes / interfaces you’ll probably want to specify what kind of exception is thrown under certain conditions. Contract.Requires<TException> helps you achieving this – TException is the type of the exception which will be thrown. As on the non-generic version you may additionally pass a message describing the reason for the exception. However, you can not fully control the thrown exception – Code Contracts will always use a constructor expecting a string as an argument. Currently, it is not possible to pass other constructor arguments using the Contract class. If you want to influence this behavior, you will have to use the so called “Legacy-Requires” connected with a Contract.EndContractBlock() – I will talk about this in the part after the next one again.

Postconditions

The method responsible for checking postconditions is Contract.Ensures.

As mentioned before, the postconditions are specified before the code which is going to fulfill them. Usually this is after the preconditions have been specified.

In opposite to Contract.Requires, Contract.Ensures provides no overload accepting a generic parameter. Such an overload would make no sense as postconditions failures should never cause exceptions.

A very simple sample:

public void Bar(IList<string> list)
{
    Contract.Ensures(list.Count != 0);

    list.Add("Hello World");
}

Result, ValueAtReturn and OldValue

Three methods of the Contract class help us formulating our postconditions: Contract.Result<T>(), Contract.ValueAtReturn(out value) and Contract.OldValue<T>(T value). While the first one represents the result of the method ValueAtReturn can be used for postcondition based on parameters passed using the out keyword. Otherwise an access to such a variable would cause a compiler error that an uninitialized variable is accessed. OldValue is used to access the value of a variable it had when entering the method.

Two little little samples:

public int Bar(IList<string> list)
{
    Contract.Ensures(list.Count == (Contract.OldValue(list.Count) + 1));
    Contract.Ensures(Contract.Result<int>() >= 0
                     && Contract.Result<int>() < list.Count);
    Contract.Ensures(list.Contains("Hello World");
    Contract.Ensures(Contract.Result<int>() == list.IndexOf("Hello World"));

    list.Add("Hello World");
}

public void Bar(out bool test)
{
    Contract.Ensures(Contract.ValueAtReturn(out test));

    test = true;
}

Assert /Assume

Contract.Assert and Contract.Assume are similar to Debug/Trace.Assert. There is no difference in their usage. However, they can be configured using the Code Contract settings pane. Contract.Assert, in addition, is included in static checking which will be covered in a later posting.

public void Bar(IList<string> list)
{
    Contract.Requires(list.Contains("Foo"));

    int index = list.IndexOf("Foo");
    Contract.Assert(index >= 0 && index < list.Count);
}

Contract.EnsuresOnThrow

Similar to Contract.Ensures, Contract.EnsuresOnThrow<TException> specifies postconditions. They, however, have to be fulfilled when TException is thrown.

Little sample:

public void Bar(string file)
{
    Contract.EnsuresOnThrow<FileNotFoundException>(!File.Exists(file));

    File.OpenRead(file);
}

Conclusion / Outlook

Code Contracts are proper installed on our system. We got our first look on them and are able to specify first pre- and postconditions using them.

The next part will introduce Object Invariants, later we will see how to specify all this for abstract classes and interfaces.

DotNetKicks Image
About these ads

One Response to “No Interface Without Contract? – Part 5: Using Microsoft Code Contracts”

  1. DotNetShoutout Says:

    No Interface Without Contract? – Using Microsoft Code Contracts…

    Thank you for submitting this cool story – Trackback from DotNetShoutout…


Comments are closed.

Follow

Get every new post delivered to your Inbox.

%d bloggers like this: