Code Contracts #1: Basic information

During the last days and weeks, I’ve had the chance to make my mind up on Code Contracts, validation vs. verification of code and code quality on the whole. I’ve made some examples with Code Contracts and want to start a basic blog post series here, which should give you some further information on this. Code Contracts as project are not baked, yet. Thus I don’t throw with mud about things, that will definitely work in the future. This makes no sense! I just want to share some knowledge and want to know what you think about this altogether.

„Code Contracts“ is a project from the Microsoft DevLabs (http://msdn.microsoft.com/en-us/devlabs/dd491992.aspx) and can be downloaded and installed in a very early state at the moment. The origin of Code Contracts is the programming language Spec#, which is extending C# at aspects for definition of conditions, that have to be fulfilled by part of a programmer’s code (classes, methods, variables, …). Moreover, the „Code Contracts Library“ has been decoupled from Spec# for Code Contracts and has been modified to work with the .NET framework in general. Thus, Spec# as research project has served its time, but it’s living on with Code Contracts. The impact of Code Contracts is not to underestimate: the component is going to be an element of the .NET 4.0 class library and thus it’s making its way into all .NET based languages.

But what’s hiding behind Code Contracts? The idea is the same as in Spec#: taking your code under contract, that means setting conditions on it. The programmer then has to take care about fulfilling those conditions (contracts) with his code. This idea isn’t new at all, since it comes originally from the Eiffel programming language, which has been introduced in 1985 already. Therefore Eiffel supports the Design by Contract (DbC) principle, whereby the following aspects can be defined in the code:

• pre-conditions: Those are declared on method level and define conditions, which have to be fulfilled at entrance of a method (that means which contracts have to be kept by the caller). Mainly, these are conditions on method parameters (e.g. prohibition of null-values).
• post-conditions: Those are declared on method level, too and define conditions, that have to be fulfilled at exit of a method (meaning contracts, that the method’s code has to ensure). For example, one could make conditions on the return value, that callers of the method could rely on.
• invariants: Those are definitions on class level, depicting conditions, that have to be fulfilled at exit of any method of the class. For example, one could define conditions on the value of fields or properties of the class (be not null, be positive, have a defined value range, etc.).

The following example of a method deposit for a banking account illustrates the use of pre- and post-conditions in their original language Eiffel:

deposit (amount: INTEGER) is
    require
        non_negative: amount > 0
    do
        balance := balance + amount
    ensure
        updated: balance = old balance + amount
end

Pre-conditions can be defined with require, ensure defines post-conditions, that have to be true at exit of the method. Those can also describe the value of class members as shown in this (trivial) example for the member balance. Thereby, Eiffel is checking at runtime if the contracts are fulfilled and if not it’s notifying with an error.

Just those definitions are possible with Code Contracts in .NET, too. With static methods on the newly introduced class Contracts, the programmer gets the possibility to define such contracts. The deposit method from the example above would look in .NET Code Contracts as follows:

public void Deposit(int amount)
{
    Contract.Requires(amount > 0);
    Contract.Ensures(Balance == Contract.OldValue(Balance) + amount);

    Balance += amount;
}

With Contract.Requires() one can define pre-conditions, with Contract.Ensures() post-conditions. Contract.OldValue() can be used in a post-condition and is a placeholder for the value of a variable on class level (property, field) at entrance of the method.

To use Code Contracts in your own projects and get first insights, you have to download the current package from http://msdn.microsoft.com/en-us/devlabs/dd491992.aspx and install it. Then, if you add a reference to the Microsoft.Contracts.dll to your project, you can access the Contract class from the namespace System.Diagnostics.Contracts. But again as reminder: the Code Contracts project is in an early state at the moment, so don’t expect a perfect solution. The team is working hard to improve their code and thus everybody should appreciate their work. Many things have to be done until the rise of .NET 4.0, but I’m sure that they’ll do their job very well.

Those are first basic information about Code Contracts. Next blog posts will involve deeper knowledge about Code Contracts, the components of Code Contracts, more examples and information about why it makes a change and why one should care about.