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
<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.
Ira Lukhezo's blog 
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.