Learn about Code Contracts in .NET Framework 4.0

Introduction

In this article we will show you how to utilize Code Contracts in the .NET framework 4.0 using the Design By Contract principle. Code Contracts are included in the .NET framework 4.0 base class libraries by default. If you are using the .NET 3.5 framework then you may have to download it separately.

For our discussion, we are going to use the code contracts with .NET framework 4.0--we won't be focusing on previous versions.

Code Contracts in .NET Framework 4.0

As the name indicates, code contracts are used to define contracts like validating the method input parameter values, method return values or other class member values. They are also used to make sure that the caller abides to the contracts that your implementation class has provided. Code contracts come in really useful when you are building large scale re-usable components, and enables you to achieve the design-by-contract principle. Below is the excerpt from Wikipedia on the design-by-contract principle.

Design by Contract (DbC) or Programming by Contract is an approach to designing computer software. It prescribes that software designers should define formal, precise and verifiable interface specifications for software components, which extend the ordinary definition of abstract data types with preconditions, postconditions and invariants. These specifications are referred to as "contracts", in accordance with a conceptual metaphor with the conditions and obligations of business contracts.

Code Contract classes exist in the .NET framework under the namespace System.Diagnostics.Contracts. In code contracts there are three ways of defining contracts. They are listed below:

1. Pre-Condition - The contract condition is validated prior to the execution of the method. The Contract.Requires method helps in creating a pre-condition.
2. Post-Condition - Ensures the validity after the execution of the method code. Contract.Ensures helps in creating a post-condition. Even if the ensures statement is placed at the beginning of a method for the post-condition to modify the IL to perform the contract validation, after all is said and done, the method code gets executed.
3. Invariants - Invariants are the contract which should always evaluate to true before and after the execution of the code.

The information above will be much easier to understand when you take a look at the sample code provided below.

Having mentioned the types of contracts, now comes the question of when these contracts would be invoked.

1. Static Checking - The check is made during the compile time and the messages are displayed as warnings.
2. Runtime Checking - The check is made during the runtime and the messages are thrown as exceptions.

Go to properties of the project and select Code Contracts tab. Select the options based on the needs as shown in Fig 1.0 below:

Fig 1.0

An Explanation Using Code Samples

In this section I will provide the sample code. Create a Console application using Visual Studio 2010 and .NET framework 4.0. Name it CodeContractsSample. In the Program.cs file, place the code shown below:

namespace CodeContractsSample
{
    class Program
    {
        static void Main(string[] args)
        {
            CalculatorPreCondition preCondition = new CalculatorPreCondition();
            preCondition.Add(7, 101);

            CalculatorPostCondition postCondition = new CalculatorPostCondition();
            postCondition.Add(20, 120);

            CalculatorInvariant invariant = new CalculatorInvariant();
            invariant.Value1 = 100;
            invariant.Value2 = 20;
            invariant.Sub();
        }
    }

    public class CalculatorPreCondition
    {
        public int Add(int value1, int value2)
        {
            //Check for the parameter validation using precondition
            Contract.Requires(value1 > 10, "Value 1 should be greater than 10");
            Contract.Requires(value2 > 100, "Value 2 should be less than 100");

            return value1 + value2;
        }
    }

    public class CalculatorPostCondition
    {
        int value3 = 0;
        public int Add(int value1, int value2)
        {
            //Check for the return value using post condition
            //Post-condition would work even though the ensures statement is
            //placed above the line where the actual value for Value3 is set.
            Contract.Ensures(value3 < 110, "Value 3 should be less than 110");

            return value3 = value1 + value2;
        }
    }

    public class CalculatorInvariant
    {
        public int Value1 { get; set; }
        public int Value2 { get; set; }
        public int Sub()
        {
            return Value1 - Value2;
        }

        [ContractInvariantMethod]
        private void ContractInvariant()
        {
            Contract.Invariant(this.Value1 > this.Value2, "Value 1 should always be greater than Value 2");
        }
    }
}

Now enable both static and runtime checking. Fig 2.0 below shows the warnings displayed during compilation as a result of static checking.

Fig 2.0

If you run the application you will notice the exception messages in the Console window as shown in Fig 2.1 below.

Fig 2.1

Conclusion

I hope this article clearly highlights the use of code contracts in the .NET framework and how it becomes so handy when building components and applications through the design-by-contract principle. Please make use of the comments section below to provide your valuable comments.