Code Contracts forthcoming in Visual Studio 2010 and .NET 4.0


I am really excited that Code Contracts are etched in to be added to the Base Class Library in .NET 4.0. This abundant excitation is genuine, so-much-so I got up at an ungodly hour this morning, planning, scheming and envisaging getting my hands on the new Library.

Code Contracts allow you to express preconditions, postconditions and object invariants in your code for runtime checking, static analysis, and documentation. You may be aware of background compilation that was added to the C# compiler in Visual Studio 2008 SP1. This is a real advance for static type languages like C# and Visual Basic, because you can start to be explicit about how your code will behave, as it is written, and errors caught even before you compile the program.

Presently, imperative programming languages are ill equipped to deal with the issue of concurrency, and the many core shift in personal computers. One of the chief obstacles in designing parallel code, is the issue of side effects. Contracts don’t offer the benefits of functional programming per se, but they do make your code more easier to predict, which is going to be a key tool in development going forward, as I don’t see all the imperative programmers in the world, and billions of lines of imperative code suddenly being converted into functional code.

The best way to demonstrate this, is through an example. Before that though, feel free to download the Code Contracts library from Microsoft Research. Presently, I am using the academic license which works with Visual Studio Professional, if you do choose to use the commercial license, you will need Visual Studio 2008 Team System. You also want to download the documentation from here, and keep an eye out for developments at the BCL Team blog.

Note: This tutorial is in both C# and Visual Basic

Common Problem

I have a simple class, that demonstrates very well (however simple it might be) what happens in real world development, pretty much on a daily basis. I am creating a class called Rational (go here if you don’t know what a rational number is) , instantiating it, and passing in a couple of values. What you you think happens when I hit F5 to run the program?

Visual Basic

Module Module1

    ‘ Simple class to represent rational numbers

    Public Class Rational

        Private numerator As Integer

        Private denominator As Integer

 

        Public Sub New(ByVal numerator As Integer, ByVal denominator As Integer)

            Me.numerator = numerator

            Me.denominator = denominator

        End Sub

 

        ‘ Method returns the closest integer by truncation

        Public Function ToInt() As Integer

            Return Me.numerator / Me.denominator

        End Function

    End Class

 

    Sub Main()

        Dim rational As New Rational(3, 0)

        Console.WriteLine(rational.ToInt())

    End Sub

 

End Module

C#

using System;

using System.Diagnostics.Contracts;

 

namespace CodeContractsDemo

{

   // Simple class to represent rational numbers

    public class Rational

    {

        int numerator;

        int denominator;

 

        public Rational(int numerator, int denominator)

        {

            this.numerator = numerator;

            this.denominator = denominator;

        }

 

        // Method returns the closest integer by truncation

        public int ToInt()

        {

            return this.numerator / this.denominator;

        }

 

    }

    class Program

    {

        static void Main(string[] args)

        {

            Rational rational = new Rational(3,0);

            Console.WriteLine(rational.ToInt());

 

        }

    }

}

 

Well you guessed it!

Visual Basic Error

OverflowException

 

C# Error

DivideByZeroException

This is such a frequent programming mistake, whereby parameters are added that end up causing problems further down the line. Who knows how long it has been since the rational class was first created, and the operation of passing in the zero denominator?

Note: When you installed Code Contracts from Devlabs, the necessary .dll was added to your machine. In C# right click the references node in Solution Explorer and go to add a reference (In Visual Basic double click MyProject in Solution Explorer and select the References tab on the left and select add) to Microsoft.Contracts Library. This will be included in MSCORLIB in .NET 4.0.

ContractsLibrary

You should now find that you can include the System.Diagnostics.Contracts namespace to the top of your class

Visual Basic

Imports System.Diagnostics.Contracts

C#

using System.Diagnostics.Contracts;

Code Contracts

Code Contracts are designed to preclude such eventualities from ever occurring in the first place, and to prevent them really early on, without the need to run the program first. This in some ways illustrates the limits of background compilation, which itself is not a limitation, but the point of inflexion whereby a developer starts to create an algorithm. The background compiler cannot deduce what a developer wants to do beforehand, if it could, we’d all be out of a job.

I need a way to disallow the client from ever passing in a zero denominator. Typically, today, I would write some parameter validation code in the constructor, that throws an exception.

Add the following code to the constructor of the class above (I have decided I want just positive numbers now)

Visual Basic

     Public Sub New(ByVal numerator As Integer, ByVal denominator As Integer)

            Contract.Requires(0 < denominator)

            Me.numerator = numerator

            Me.denominator = denominator

        End Sub

C#

      public Rational(int numerator, int denominator)

        {

            Contract.Requires(0 < denominator);

            this.numerator = numerator;

            this.denominator = denominator;

        }

When you installed the contracts library, a new Code Contracts tab was added to your project. In C# double click the Properties node in Solution Explorer in Visual Basic, double click MyProject in Solution Explorer

VisualStudio

Place a check in the “Perform Runtime Contract Checking” checkbox, return to the project and hit F5 to run the project.

You should find you have the following (Note: the failure is a Precondition)

PreCondition

This Debug.Assert is called upon instantiation of the class, and does not occur further down the line when ToInt() is called.

Return to the Code Contracts tab, and this time check “Perform Static Contract Checking” and build

StaticAsWell

You should now find that you have warnings in your error list

Visual Basic

VBError

C#

CSharpError

You don’t need to execute your code, the static checker runs a build time which is pretty smart. It is a best practice to always enable runtime checking as well, as the static checker does not always catch every single error, but the real power in this, is that every precondition in the solution is checked.

Change the zero parameter in the constructor thus, and build

Visual Basic

    Sub Main()

        Dim rational As New Rational(3, 4)

        Console.WriteLine(rational.ToInt())

    End Sub

C#

     static void Main(string[] args)

        {

            Rational rational = new Rational(3, 4);

            Console.WriteLine(rational.ToInt());         

        }

It is still possible for a zero denominator to enter the ToInt() method, even though it appears impossible due to the constructor code. One might have another method in this class or have sub types of this class, and there is nothing to prevent this Rational class from getting a zero denominator even though the class was not created with a zero in the first place. The way one protects the class from this occurring is through an object invariant method.

In the code editor type “cim” and then tab tab – just like adding an event handler (no code snippets yet in the VB editor)

ContractInvariantMethod 

Visual Basic

     <ContractInvariantMethod()> _

        Protected Sub ObjectInvariant()

            Contract.Invariant(False)

        End Sub

C#

      [ContractInvariantMethod]

        protected void ObjectInvariant()

        {

            Contract.Invariant(false);

        }

 

You can then set the parameter in the method

Visual Basic

        <ContractInvariantMethod()> _

        Protected Sub ObjectInvariant()

            Contract.Invariant(Me.denominator > 0)

        End Sub

C#

   [ContractInvariantMethod]

        protected void ObjectInvariant()

        {

            Contract.Invariant(this.denominator > 0);

        }

It is now impossible for the denominator in the class to ever be zero. One also want to be able to inform clients of this Rational class what the ToInt() returns, this is the postcondition.

Visual Basic

        ‘ Method returns the closest integer by truncation

        Public Function ToInt() As Integer

            Contract.Ensures(Contract.Result(Of Integer)() >= 0)

            Return Me.numerator / Me.denominator

        End Function

C#

        // Method returns the closest integer by truncation

        public int ToInt()

        {

            Contract.Ensures(Contract.Result<int>() >= 0);

            return this.numerator / this.denominator;

        }

The thing to notice here is that the Contract.Ensures method is declared before the integer is returned, but the compiler (magic) rearranges the code so this code is called after the integer has been returned back. I will now show the completed projects showing preconditions, object invariants and postconditions.

Visual Basic

Imports System.Diagnostics.Contracts

 

Module Module1

    ‘ Simple class to represent rational numbers

    Public Class Rational

        Private numerator As Integer

        Private denominator As Integer

 

        Public Sub New(ByVal numerator As Integer, ByVal denominator As Integer)

            Contract.Requires(0 < denominator)

            Contract.Requires(0 <= numerator)

            Me.numerator = numerator

            Me.denominator = denominator

        End Sub

 

        <ContractInvariantMethod()> _

        Protected Sub ObjectInvariant()

            Contract.Invariant(Me.denominator > 0)

            Contract.Invariant(Me.numerator >= 0)

        End Sub

 

 

        ‘ Method returns the closest integer by truncation

        Public Function ToInt() As Integer

            Contract.Ensures(Contract.Result(Of Integer)() >= 0)

            Return Me.numerator / Me.denominator

        End Function

 

    End Class

 

    Sub Main()

        Dim rational As New Rational(12, 3)

        Console.WriteLine(rational.ToInt())

    End Sub

 

End Module

C#

using System;

using System.Diagnostics.Contracts;

 

namespace CodeContractsDemo

{

   // Simple class to represent rational numbers

    public class Rational

    {

        int numerator;

        int denominator;

 

        public Rational(int numerator, int denominator)

        {

            Contract.Requires(0 < denominator);

            Contract.Requires(0 <= numerator);

 

            this.numerator = numerator;

            this.denominator = denominator;

        }

 

        [ContractInvariantMethod]

        protected void ObjectInvariant()

        {

            Contract.Invariant(this.denominator > 0);

            Contract.Invariant(this.numerator >= 0);

        }

 

 

        // Method returns the closest integer by truncation

        public int ToInt()

        {

            Contract.Ensures(Contract.Result<int>() >= 0);

            return this.numerator / this.denominator;

        }

 

    }

    class Program

    {

        static void Main(string[] args)

        {

            Rational rational = new Rational(12,3);

            Console.WriteLine(rational.ToInt());         

        }

    }

}

 

I am sure one can be certain that you be seeing a lot more of this type of .NET code in the not too distant future.

One thought on “Code Contracts forthcoming in Visual Studio 2010 and .NET 4.0

  1. One thing to note in your example. The static checker would produce an unproven ensures in the VB sample. The ToInt method is using floating-point division rather than integer division. Since part of the Ensure is that the return will be an Integer, unless you change the method to use integer division (backslash instead of forward slash in VB) you’ll get an unproven ensures warning.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s