Code Contracts forthcoming in Visual Studio 2010 and .NET 4.0

Ira Lukhezo — Wed, 25 Feb 2009 10:26:32 +0000

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 
 
C# Error

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.

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

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)

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

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

Visual Basic

C#

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)
 
Visual Basic      _
        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

         _
        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
 
         _
        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.

Posted in Code Contracts

Spec#, a new dawn for programming languages

Ira Lukhezo — Thu, 29 May 2008 11:24:58 +0000

Spec# pronounced ‘Spec Sharp’ is new attempt at a more cost effective way to develop and maintain high-quality software. This language is being developed by Microsoft Research and has left me completely dumbstruck. My favourite programming language is C# of which I’m self taught, but I was formally trained in C/C++.

Spec# is an extension to C# that introduces the notion of contract based programming. If you have tried Windows Communication Foundation, you will be familiar with the notion of contracts. Spec# takes things to a whole new level, and is very very explicit – this is a complete understatement by the way.

When you are defining your encapsulated fields and methods you have to go into a great more detail about how those fields and methods will operate, all at compile time. In C++, C# or Visual Basic, a developer usually writes a chunk of code and then compiles that code into a .dll or executable. It is only at this stage when problems are identified, and resolutions are effected. Spec# does not allow this because as you write your code it checks everything. One of the key features is that you have to specify values as non-null. This is a big deal.

What non-null stipulations allow for, is very performant code (‘performant’ is a word used by Technical Fellows so it is now a word – as far as I am concerned). This is because code is not being checked for being null which is something that is always done for Common Language Runtime languages. The way the Spec# team achieve this is through their ‘brain-box’ knowledge of Microsoft Intermediate Language.

I will certainly be keeping my eyes on this one.

Ira Lukhezo's blog » Search Results » code+contracts

Code Contracts forthcoming in Visual Studio 2010 and .NET 4.0

Common Problem

Visual Basic

C#

Visual Basic Error

C# Error

Visual Basic

C#

Code Contracts

Visual Basic

C#

Visual Basic

C#

Visual Basic

C#

Visual Basic

C#

Visual Basic

C#

Visual Basic

C#

Visual Basic

C#

Spec#, a new dawn for programming languages