Posts Tagged ‘precondition’

Hello all,

This time we’ll do a quick exploration of how we can apply Code Contracts to interfaces. As you know from our post First Steps with Code Contracts, the preconditions and postconditions (Contract.Requires and Contract.Ensures calls, respectively) must be placed inside a method body.

Therefore, when defining an interface, we run into a problem: We do not have method bodies there. Of course we could put such calls inside each effective implementation of the interface methods. Clearly, this is not what we want, since

  • We do not want to replicate code in x classes that implement our interface and
  • Future implementations of our interface would contain the conditions we need

Luckily, the Code Contracts provide us with a powerful mechanism that allows us to define a class which implements that interface and which will do the necessary checks.

The Contract Class

Let’s see how this is done, right? For this example, please recall our example from the First Steps with Code Contracts introductory article.


   1: namespace Vehicles

   2: {

   3:     interface IVehicle

   4:     {

   5:         void Drive(Int32 speed);        

   6:     }

   7: }

Snippet 1: The IVehicle interface

Also do recall that we did not define any pre- or postconditions for our interface (how could we? – there is no method body).

This is exactly the place, where we will put a so called Contract Class, that will implement our interface. Every time the interface is called, the conditions put into our Contract Class will be injected. This holds for every implementation of our interface.

We basically need two things:

1. A class that implements our interface IVehicle that is marked as Contract Class via an attribute:


   1: [ContractClassFor(typeof(IVehicle))]

   2: public class IVehicleContract : IVehicle

   3: {

   4: }

Snippet 2: Contract Class implementing the interface we want to fulfil requirements

2. Another class that links up our interface to the ContractClass

   1: [ContractClass(typeof(IVehicleContract))]

   2: public partial interface IVehicle

   3: {

   4: }

Snippet 3: The link between the interface and our Contract Class

Hint: Don’t worry: You do not have to implement these two classes from scratch: The Code Contracts come with a bunch of predefined snippets that can be executed right away. The following snippet will do the trick for generating the Contract Classes for an interface:


cintf ->(TAB – TAB)

The next step is to implement the interface for IVehicleContract.


Figure 1: Explicitly implementing the interface IVehicle for the IVehicleContract class.

The result is shown in Snippet 4:

   1: [ContractClassFor(typeof(IVehicle))]

   2: public class IVehicleContract : IVehicle

   3: {

   4:     void IVehicle.Drive(int speed)

   5:     {

   6:         throw new NotImplementedException();

   7:     }

   8: }

As a next step, we can implement our conditions in the method body of IVehicle.Drive method in IVehicleContract, like shown in Snippet 5:

   1: [ContractClassFor(typeof(IVehicle))]

   2: public class IVehicleContract : IVehicle

   3: {

   4:     void IVehicle.Drive(int speed)

   5:     {

   6:         Contract.Requires(speed >= 0);

   7:     }

   8: }

Snippet 5: precondition in interface method implementation.

What does this mean now? Well, for every implementation of the interface IVehicle , the code precondition will be injected. In other words:


The condition we define in the Contract Class must hold for all implementations of the interface.


That was it already (for this time)! It is as simple to use as it seems.


Enjoy and stay tuned for the next time!

Best regards,


Read Full Post »

Hello all,

Today we are going to talk about another exciting project from the Microsoft Research Labs: Code Contracts. It is a Design-By-Contract (DbC) system, that enables us as developers to formulate the expected behaviour of our code by directly putting it into the code.

The main tools of applying Code Contracts are:

  • Static checking (checks contracts at compile time)
  • Runtime checking (checks contracts at runtime)
  • Automated documentation generation (keeps code and docs in sync)


Before we get started using Code Contracts. I used the following environment for carrying out the tests with Code Contracts:

  • Windows 7
  • Visual Studio 2010 Beta 2 Ultimate*
  • Code Contracts Tools*

Important: I used Visual Studio 2010 Beta 2, because it contains the .NET framework 4, which already includes the Code Contracts framework. You could also use them with VS2008, if you installed the .NET framework 4. The Code Contract Tools need to be downloaded separately. I highly recommend them, since they will add a new pane to your VS2010 which in turn lets you set various options, like enabling the static checker directly from the UI.

1.1 The Strengths of Code Contracts

Elevating assertions to the API level. At this point, the specification of code is not only somewhere deeply hidden in the method, but immediately visible to the caller (if, for example, a Contract is not fulfilled). On the other side, a caller now can know perfectly what to expect from a method.

1.2 Code Contracts for Methods

First, we are going to show how to implement Code Contracts on the method level.

We’ll start with the creation of a test project that will serve our purposes of showing Code Contracts’ capabilities:


Figure 1: Add a new console application and name it Vehicles

As a next step, we create a class and an interface, namely Car and IVehicle. Implement them as follows in the snippets 1 and 2. Leave the automatically generated Program class – we’ll need it later for running our examples.

   1: using System;

   2: using System.Collections.Generic;

   3: using System.Linq;

   4: using System.Text;


   6: namespace Vehicles

   7: {

   8:     interface IVehicle

   9:     {

  10:         void Drive(Int32 speed);

  11:     }

  12: }

Snippet 1: Interface IVehicle, defining one method signature

   1: namespace Vehicles

   2: {

   3:     class Car : IVehicle

   4:     {

   5:         string name;

   6:         int speed;


   8:         public Car(string name, int speed)

   9:         {

  10:             this.name = name.ToUpper();

  11:             this.speed = speed;

  12:         }


  14:         void IVehicle.Drive(int speed)

  15:         {

  16:             Console.WriteLine("Car " + name +

  17:             " is driving at a speed of " + speed);

  18:         }


  20:         public bool IsFasterThan(Car c2)

  21:         {

  22:             Console.WriteLine(name.ToUpper() +

  23:             " is faster than "

  24:             + c2.name.ToUpper());


  26:             if (this.speed > c2.speed)

  27:                 return true;

  28:             else return false;

  29:         }

  30:     }

  31: }

Snippet 2: Class Car implementing IVehicle.

So far, so good, right? Nothing special there, and the code has got very simple “functionality”. A car that can drive, alright. And check whether it is faster than another car. Compiling the project reveals a succeeding build which at first sight contains no errors.

Before we take further steps, let’s activate the Static Checking feature of Code Contracts. In order to enable this, just right-click the project Vehicles -> Properties.

The last pane on the bottom of the Properties’ window is called Code Contracts. Go for it.


Figure 2: The Code Contracts’ configuration in Properties. Then proceed with Figure 3.


Figure 3: Enable static contract checking and the checking of implicit non-null obligations.

Compile again, and in the warning sections, we’ll receive a bunch of warnings generated by Code Contracts:


Figure 4: Warning list, generated by Code Contracts.

Those messages are suggestions of how we should change our code in order to be (more likely to be) safe from exceptions.

The warnings, line by line:

1-2: Tell us that we should add a pre-condition in order to be sure from NullReferenceExceptions when accessing the property name (1) or passing a parameter that could be possible equal to null (2). The cool thing is: Code Contracts even provide us with the correct code in order to achieve this.

3-5: These are the actual warnings, containing possible failures.


A precondition is simply added by using the following method:


When debugging, we can step over such a call and verify that it is actually executed. The call is made in the method body, at any desired position. Usually it is placed at the beginning.


A postcondition is simply added by using the following method:


When debugging, we cannot step over such a call (to be precise: not at the position where we put it in the code), since it is not actually executed in the method body, but only afterwards. Once we stepped over the complete method, we arrive at the Contract.Ensures call. The following snippet show how pre- and postconditions can be applied to the methods of our class Car:

   1: using System;

   2: using System.Collections.Generic;

   3: using System.Linq;

   4: using System.Text;

   5: using System.Diagnostics.Contracts;


   7: namespace Vehicles

   8: {

   9:     class Car : IVehicle

  10:     {

  11:         string name;

  12:         int speed;


  14:         public Car(string name, int speed)

  15:         {

  16:             Contract.Requires(name != null);

  17:             this.name = name.ToUpper();

  18:             this.speed = speed;

  19:         }


  21:         void IVehicle.Drive(int speed)

  22:         {

  23:             Console.WriteLine("Car " + name +

  24:             "is driving at a speed of " + speed);

  25:         }


  27:         public bool IsFasterThan(Car c2)

  28:         {

  29:             Contract.Requires(c2 != null);

  30:             Console.WriteLine(name.ToUpper() +

  31:             " is faster than " +

  32:             c2.name.ToUpper());


  34:             if (this.speed > c2.speed)

  35:                 return true;

  36:             else return false;

  37:         }

  38:     }

  39: }

Snippet 3: The Car class, using Code Contracts’ preconditions

After we added the Contract.Requires calls in IsFasterThan and in the Car ctor, we receive only 2 warnings from Code Contracts. Just compile to verify that.

Why still two warnings? We added preconditions to check that!

The reason: Only our method IsFasterThan in this particular class, Car, requires name to be non-null. But we could have for example a subclass inheriting from Car, which does not perform the same check. Hence, we need to take care for that. And in fact, Code Contracts provides us the necessary means in order to ensure that no object deriving from Car, can have name which is null:

   1: [ContractInvariantMethod]

   2: void ObjectInvariant()

   3: {

   4:     Contract.Invariant(name != null);

   5: }

Snippet 4: Object invariants

Calling again reveals that the warning concerning the name variable of class Car has gone. Good! It means, we are safe from accessing a null value – variable, and all other programmers subclassing our Car are safe, too!

This is it for now! Next time we’ll see how to deal with Code Contracts and interfaces.

Enjoy playing with Code Contracts and see you soon!

Best regards,


Read Full Post »