Introduction

Code contracts allow one to specify the behavior of an algorithm by explicitly adhering to a well defined contract. Commonly, these contracts are in the form of pre- and post-conditions. Further, one can also specify behavioral contracts for a type in the form of a type invariant. For now you need not worry about how such contracts can be defined (we will discuss that later), however, it is important to understand some of the benefits of using code contracts, these include:

• provide high-level behavioral description of an algorithm;
• force programmers to be explicit about the behavior of their algorithms;
• help catch bugs early.

For many readers code contracts will not be a new concept, most likely you will have seen them before in texts on data structures and algorithms [2]. However, most readers will be new to applying similar concepts to their actual codebase.

In this article we will cover code contracts using Spec#, the code contracts library shipping with .NET 4.0, and finish with a lo ok at VC++ source code annotations.

Spec #

Spec# is a Microsoft Research project that extends the C# 2 .0 language so that you can easily define code contracts. In addition, Spec# also provides compile-time checks to verify certain assertions hold, e.g. that a non-null object is passed to an algorithm. In this section we will look at some of the features that the Spec# language introduced.

Pre-Conditions

Pre-conditions define the properties that an algorithm requires to be satisfied in order to operate correctly; these properties are defined by the algorithm designer. For example, a pre-condition for an algorithm that takes a single list argument could be: verify that the number of items in l is greater than 0. If any of the pre-conditions are not satisfied then the algorithm should not execute, after all if it were to execute who knows what the behavior of the algorithm would be? Certainly, the algorithm designer never intended it to be used in such a manner. The behavior would be undefined which encompasses several things, amongst them - failure.

For our first example we will look at how we can define a non-null constraint for an algorithm argument.

In the previous code listing we simply added an ! after the argument type to define a non-null constraint, this constraint is checked at compile-time by the Spec# compiler. A simple, yet powerful extension to the C# language. When applying the same constraint to a type member we must use an object initializer for that member. The object intializer syntax is similar to that found in C++.

Like non-null constraints, specifying pre-conditions in the Spec# language is very unobtrusive.

In the previous example we make use of the requires keyword introduced by Spec# to define a pre-condition. If the pre-condition is not satisfied then by default a RequiresViolationException will be thrown, we can override the default exception type by using another Spec# keyword - otherwise.

Post-Conditions

Post-conditions are used to ensure that certain properties will be met upon completion of an algorithm. For example, for an algorithm that increments its integer argument i, one could specify the following post-condition: I will ensure upon completion that the value of i will be one greater than its previous value.

In the previous code listing we use the Spec# keyword ensures to define the post-condition. We also make use of the special function old to acquire the original value of i passed to the algorithm. We can use the Spec# throws keyword to specify the type of exception to throw upon failure to satisfy a post-condition.

Type Invariants

To conclude our exploration of the Spec# language we will look at how one specifies type invariants. A type invariant is a property that must hold throughout the lifetime of an object, if the property fails to hold then the state of the object is deemed invalid. For example, specifying that the value of the m_count member within the List data structure should never be negative is a type invariant.

In the previous code listing we use the Spec# keyword invariant to specify a type invariant for the List data structure.

We have only covered a small amount of what the Spec# language offers in this section, for more see [1, 3, 4].

.NET Code Contracts

In this section we will take a look at the code contracts library which will be shipped with .NET 4.0 framework. All the code in this section is based on the February 2009 code contracts preview.

The functionality that we will cover of the code contracts library are:

• pre-conditions;
• post-conditions; and
• type invariants.

The associated tooling that ships with the code contracts library includes the ability to verify contracts at compile-time, as well as runtime checking. Further, the contracts specified can also be used to drive XML documentation.

Tooling to enable the generation of documentation from the code contracts specified is penned for a future release. You might want to check out the following URL for more information on future tooling - http://blogs.msdn.com/bclteam/archive/2008/11/11/introduction-to-code-contracts-melitta-andersen.aspx

All of the methods required can be found in the System.Diagnostics.Contracts namespace. You will need to reference the Microsoft.Contracts.dll found in the install directory of the code contracts preview from your project.

Before we look at some code we need to talk about a few property options that you can define. These properties can be defined by selecting the Code Contracts tab within the properties page of your C# project. We will look at two of the available properties in this article. The first property, Runtime Checking allows us to enable the runtime checking of pre-conditions, post-conditions, and type invariants. The second property, Static Checking allows us to specify whether or not we want certain properties of our program to be checked at compile-time. For all the code listed in this section assume that we are using a debug build and that the following options are checked within the Code Contracts tab:

• Runtime checking – Perform Runtime Contract Checking (defines CONTRACTS FULL constant)
• Static Checking – Perform Static Contract Checking - Implicit Non-Null Obligations

There are two tools that will be invoked now during a build of our code:

• ccrewrite: rewrites the binary and injects code at the correct position, e.g. post-conditions will be injected just before a method exit.
• ccchecker: is a static checker to verify the conditions specified in the Static Checking properties tab.

The two tools are not dependent on one another so depending on the options you define within your project properties then the correct tool(s) will be invoked during a build.

Pre-Conditions

Just like in the Spec# section we will start by defining a non-null constraint, remember though that as we have static checking enabled we expect this precondition to be verified at compile-time.

In the previous code listing we use the static method CodeContract.Requires to specify our pre-condition. If you build the code listing you will see that a warning is flagged with the textual description “requires is false”.

For our second example we will define a pre-condition that will not be flagged by the ccchecker tool, rather we will rely on the runtime verification code produced by ccrewrite.

If you build the previous code listing then you will notice that the ccchecker tool does not complain about the pre-condition of MyAlgorithm not being satisfied. However, if you run the code an unhandled exception window will be presented alerting us that the pre-condition was not satisfied.

Post-Conditions

Post-conditions using the co de contracts library are simple to define. Moreover, the library provides a host of methods which allow for easy access to certain properties of an algorithm. The following code listing demonstrates the specification of a post-condition with the aid of some special methods exposed by the code contracts library.

In the previous code listing we make use of two special methods exposed by the co de contracts library: T Contract.Result<T>() and T Contract.OldValue<T>(T value). The first method allows us to reference the actual return value of the method, the second allows us to get the pre-state value of i. If you build the previous code listing you will get another “ensures unproven” message flagged as we have not proven sufficiently that the post-condition will be satisfied. Further, if you decide to disregard the warning message and run the program then you will be greeted with an unhandled exception window reaffirming that the post-condition has not been satisfied. The fix? Well, for this simple case all we need to do is exactly what we said we would do in the post-condition, we simply increment i by one.

For brevity this will conclude our look at the post-conditions within the code contracts library. However, the reader should be informed that we have only scratched the surface with respect to post-conditions in the code contracts library. More information on post-conditions can be attained via the manual that ships with the code contracts preview download.

Type Invariants

Type invariants are easy to specify using the code contracts framework. It’s simply a matter of creating an appropriate method which will be automatically called to verify the invariant. In order to qualify, the method must:

• be public, protected, or internal;
• have a return type of void; and
• be decorated with the ContractInvariantMethod attribute.

The type invariant is checked upon all method exits and is assumed to hold upon on all method entries, this includes constructors.

In the previous code listing a type invariant is specified to ensure that the value of the member m count never has a negative value. If at any stage the type invariant fails to hold then an unhandled exception window is presented. All the type invariants you specify must be contained within the method decorated with the ContractInvariantMethod attribute.

ccrewrite

In this section we will take a look at the ccrewrite tool. The tool itself is invoked when you specify that you want to perform runtime checks to verify pre-conditions, post-conditions, and type invariants. The ccrewrite tool injects pre- and post-conditions into the correct place as well as injecting other boilerplate code. To clarify this let us consider the following method:

After ccrewrite has been invoked the previous method looks like the following:

Some things to note:

• Contract.Old() is assigned the value of i immediately upon method entry;
• a generated temporary variable now holds the value of i, the method returns this value by calling T Contract.Result<T>(); and
• ccrewrite has injected an internal class _RewriterMethods into the binary which comprises of five static methods: RewriterAssert(bool condition, string message), RewriterAssume(bool condition, string message), RewriterEnsures(bool condition, string message), RewriterInvariant(bool condition, string message), and RewriterRequires(bool condition, string message).

Also it is worth noting that wherever you place your pre- and post-conditions in your method, ccrewrite will ensure these conditions are injected at the appropriate places, e.g. pre-conditions will be injected just after method entry (only preceded by other ccrewrite boilerplate code), and post-conditions will be injected just before method exit.

I strongly advise that you become familiar with the code that ccrewrite injects into your binary. If you use code contracts liberally you will notice that ccrewrite injects an awful lot of code to help verify your contracts.

Visual C++ Source Annotations

The Microsoft VC++ 8.0 and 9.0 compilers allow you to specify pre- and post-conditions via the use of source annotations. As you might have guessed the VC++ source annotations are more low-level than those offered in the .NET 4.0 code contracts library, this is to be expected as the needs of C++ programmers differ greatly from those of their C# counterparts. Source annotations are incredibly powerful and well worth using. However, before you can use source annotations in your C++ code you must:

• include the CodeAnalysis\SourceAnnotations.h header file;
• bring the vc attributes namespace into scope; and
• specify the /analyze compiler switch which can be done via the Code Analysis tab of the project pages or via the command line to cl.exe.

The steps are slightly different when using source annotations in C code, see the following URL - http://msdn.microsoft.com/en-us/library/ms182033(VS.80).aspx

Pre-Conditions

Specifying a pre-condition using source annotations is straightforward, they take the form [Pre(Annotation Property)].

In the previous code listing we apply a pre-condition to the pWord argument stating that the pointer must not be NULL. If you build the program you will see that a warning is flagged with the textual description “Warning C6387: ’argument 1’ might be ’0’: this does not adhere to the specification for the function ’MyAlgorithm’ ”

Post-Conditions

A post-condition specified with the use of source annotations can be used to specify properties to assist the programmer calling the algorithm in question, e.g. we might specify that the programmer must always check the return value of the algorithm, or we might want to tell the programmer that the return value should not be checked against a particular value.

In the previous code listing a warning will be flagged with the textual description “Warning C6031: Return value ignored: ’MyAlgorithm’ ” The following example specifies that the caller must check the value returned by MyAlgorithm, but not check it against the value 0.

If you build the previous code listing you will notice that we no longer get a a warning about not checking the return value of MyAlgorithm. Instead, we get warned that we are checking the return value of the algorithm against a value which the algorithm designer has defined as being invalid, the following warning is raised “Return value for a call to ’MyAlgorithm’ should not be checked against ’0’ ”

To find out more about the VC++ source annotations see the Microsoft Developer Network.

Summary

This article has shown you the benefits of using contracts within your code whether it be C# or C++. We started off by looking at Spec#, then proceeded to explore the new code contracts library shipping in .NET 4.0, and finally concluded with a brief look at the VC++ source annotations.

Code contracts allow you to be more explicit about algorithm behavior, and catch potential bugs early on. Use them whenever and wherever possible.

Acknowledgements

I would like to thank Jon Skeet, Richard Mason, and Nick Wienholt for providing valuable feedback on the original draft of this article.

References

[1] The Spec# programming system: An overview, volume 3362 of LNCS, 2004. Springer.

[2] Granville Barnett and Luca Del Tongo. Data structures and algorithms: Annotated reference with examples. WWW, December 2008.

[3] Mike Barnett, Robert Deline, Manuel Fahndrich, Bart Jacobs, K. Rustan Leino, Wolfram Schulte, and Herman Venter. The spec# programming system: Challenges and directions. pages 144–152, 2008.

[4] Manuel Fhndrich K. Rustan M. Leino Mike Barnett, Rob DeLine and Wolfram Schulte. Verification of object-oriented programs with invariants. JOT, 2004.

About Granville Barnett

Granville (http://gbarnett.org) is a PhD candidate at Durham University within the Department of Computer Science. This author has published 32 articles on DotNetSlackers. View other articles or the complete profile here.