Code Contracts for .NET 4.0 - Spec# Comes Alive

As I've said in many posts before, I'm a big fan of stating your preconditions, postconditions, invariants and so on explicitly in your code through the use of contracts in the Design by Contract Parlance.  Spec# is a project that came from Microsoft Research as a language based upon C# to add Design by Contract features to the language.  I've talked extensively on the subject in the past on this blog and previous blogs of mine especially around the time of the ALT.NET Open Spaces, Seattle event back in April of this year.  The importance of making side effects well known is something that I mentioned briefly during my Approaching Functional Programming talk at KaizenConf.  To be able to express and statically verify behavior is important in regards to side effects and method purity.

One of the less talked about items from this year's Professional Developer Conference was Code Contracts for .NET.  This talk was bundled in with automated test generation with Pex for a combined talk called "Research: Contract Checking and Automated Test Generation with Pex".  In this talk, Mike Barnett, of the Spec# team was joined by Nikolai Tillmann, who is currently leading the Pex Project, and they talk about the project, Code Contracts for .NET.  I encourage you to watch the video to see how it works and the benefits of using the library.  It's been rewarding to watch how Spec# has grown in presence in recent months, especially the publicity that both Greg Young and I have given them.  Mike has done a great job with this project and I'm really excited for the future of it.

 

Code Contracts for .NET

It was announced that a subset of Spec#, the contracts library, would be included as part of the base class library in .NET 4.0.  When .NET 3.5 came out, if you opened System.Core.dll through .NET Reflector, you may have noticed that there was a namespace in there called Microsoft.Contracts.  Since that time, the Spec# team has worked with the Base Class Library team to help integrate this more thoroughly into the libraries as a language agnostic approach.  There are many decisions to be made as languages and frameworks evolve as to what goes where.  To make these features as library features allows for more rapid change and flexibility than if they were exclusive language constructs such as they were with Spec#.  After all, I want to be able to switch to languages such as F# and still have the ability to statically verify my code. 

First things first, what is Design by Contract?  It's an approach to software development that was coined by Dr. Betrand Meyer through the creation of the Eiffel language.  The main tenets of this paradigm include:

  • What does it expect? (Preconditions)
  • What does it guarantee? (Postconditions)
  • What does it maintain? (Invariants)

The idea is to have these tenets enforced programmatically through the language itself.  To this end, in the .NET framework, outside of Spec#, haven't had this available to them.  So, the Spec# team realized, that instead of the language approach, maybe they should focus on a language agnostic approach through the use of libraries, and static verification.  Now, I can feel free to use my language of choice inside the .NET framework to utilize these contracts, such as F#, C#, VB, etc.  As part of the release at PDC, we have the libraries available to us for use in Visual Studio 2008, so we'll be going through what exactly that means.

 

Getting Started

First, you need to install the Code Contracts for .NET, which you can find here.  This integrates with Visual Studio 2008 and adds an additional property window to your project files.  This gives us the ability to enforce contracts using the Microsoft.Contracts.dll.  If you look at the property page for your given project, it should look like this. 

contracts

 

As you can see, we have the ability to perform runtime checking, static contract checking with non-null obligations and array bounds automatically.  The install comes with a PDF with some documentation on how to use the library when covering preconditions, postconditions, invariants, purity and contract classes.  Let's go through a quick example of using this library.

 

Using the Library

In order to utilize contracts, you must use the CodeContract class from the System.Diagnostics.Contracts namespace.  The CodeContract has a few interesting methods worth exploring. 

Method Meaning
Assert Express contract assertions
Assume Express contract assumptions that should hold. Assume to be true or false
EndContractBlock Used to mark the end of a code contract block of if statements
Ensures Express postconditions
EnsuresOnThrow Express postconditions that abnormally terminate a method
Exists Ensure a value exists in a collection
ForAll Express constraint for each item in a collection
Invariant Express invariant constraints
OldValue Retrieve the old value from the pre-state
Requires Express preconditions
RequiresAlways Express preconditions for all build configurations
Result Get the method's return value
Throws Express exceptional postcondition
ValueAtReturn Specify out parameter value for postcondition checking

There are several attributes worth noting as well in this library as well:

Attribute Meaning
ContractClassAttribute Define a code contract class used to enforce contracts on an interface
ContractClassForAttribute Define a code contract class for a given interface
ContractInvariantMethodAttribute Used to mark a method that represents the object invariant
ContractPublicPropertyNameAttribute Used in a method contract where the method is more visible than the field
ContractVerificationAttribute Used to assume correctness of the given assembnly
PureAttribute Express method purity
RuntimeContractAttribute Added to the assembly via the rewriter to express that is has already been rewritten

As you can see here, we have a lot of goodies in here.  Let's step just through preconditions for right now.

 

Preconditions

The first item we noted in our definition of Design by Contract is what do we expect.  In this example, let's create a simple Geocoordinate value object used to hold latitude and longitude values.  There are some constraints we need to use to ensure correctness.  We need to enforce preconditions on the constructor as well as a function used to calculate the distance between two Geocoordinate classes.  Since I want this available in all build configuration, I will use the CodeContract.RequiresAlways method to define my precondition contracts.

Let's take a look at what that might look like:

public class Geocoordinate
{
    private readonly double latitude;
    private readonly double longitude;

    public Geocoordinate(double latitude, double longitude)
    {
        CodeContract.RequiresAlways(latitude <= 90.0 && latitude >= -90.0);
        CodeContract.RequiresAlways(longitude <= 180.0 && longitude >= -180.0);

        this.latitude = latitude;
        this.longitude = longitude;
    }

    [Pure]
    public double Latitude { get { return latitude; } }

    [Pure]
    public double Longitude { get { return longitude; } }

    [Pure]
    public static double GetDistance(Geocoordinate g1, Geocoordinate g2)
    {
        CodeContract.RequiresAlways(g1 != null);
        CodeContract.RequiresAlways(g2 != null);

        const double R = 3956;
        const double degreesToRadians = Math.PI / 180;

        var lon1 = g1.Longitude * degreesToRadians;
        var lat1 = g1.Latitude * degreesToRadians;
        var lon2 = g2.Longitude * degreesToRadians;
        var lat2 = g2.Latitude * degreesToRadians;

        var dlon = lon2 - lon1;
        var dlat = lat2 - lat1;
        var a = Math.Pow(Math.Sin(dlat / 2), 2) + Math.Cos(lat1) * Math.Cos(lat2) * Math.Pow(Math.Sin(dlon / 2), 2);
        var c = 2 * Math.Atan2(Math.Sqrt(a), Math.Sqrt(1 - a));
        var d = R * c;

        return d; 
    }
}
 

I also added method purity just for clarity sake.  This allows me to specify that I am not changing object state, and is quite useful for enforcement.  This makes it obvious to the caller that this method does no more than compute the result and return it.  That's important and reassuring when using third party libraries.  Let's say I call this class with the following code:

static void Main(string[] args)
{
    var g = new Geocoordinate(91.0, 181.0);
    var g1 = new Geocoordinate(40.774, 73.972);
    var g2 = new Geocoordinate(40.811, 73.910);
    var distance = Geocoordinate.GetDistance(g1, g2);
    Console.WriteLine(distance);
}
 

You may notice that the g is out of bounds from my precondition.  When I run the application, I get a nasty reminder that I broke the contract.

assert_fail

That's exactly the behavior we wanted to express through our precondition.  There is a lot more to cover in subsequent posts on the subject, but I hope this gives you a sense of some of the power of the library.

 

Wrapping It Up

This is just a first look at the new Code Contracts library.  In my talks at the Continuous Improvement in Software Development conference, I stressed the need to for our intentions to be more clear in our code.  This is a great first step to creating a language agnostic approach to static code verification.  To be able to ensure to the caller what the API will expect, return and maintain is especially powerful and I think important in the future of software development, especially in regards to state management.  The language agnostic approach given with this library is an important step forward, so that I could statically verify my code no matter the language on the .NET platform.  There is a lot more to this library to explore.  I urge you to download it, and give them feedback.  You can post feedback on the Pex forums or send them an email at codconfb _at_ microsoft _dot_ com.



kick it on DotNetKicks.com

6 Comments

  • OK, so everyone basically does this already with thinks like ArgumentOutOfRangeException - what is different now? Can the contract be determined if you don't have the source code (not relying on comments etc)?

  • Yes, because the compiler will tell you whether you violated or potentially violated the contract. That's the key that we're currently missing is the proving.

    Matt

  • Whatever became of Z Notation? :-|

  • Hi can you tell me me how to write the execption hierachy ,looks like iam missing somethng
    using System;
    using Microsoft.Contracts;
    class negativeException:ICheckedException{
    public negativeException(){
    base();
    Console.WriteLine("Wrong Value of N");

    }


    }
    public class Program
    {

    public static long findFACTORIAL(int n)
    requires n>=0 otherwise ArgumentOutOfRangeException;
    throws new negativeException();
    ensures result >0 && result<=long.MaxValue;

    {
    try{
    int fact=1;
    for(int i = 1;i<=n;i++)
    invariant i<=n;
    fact *=i;
    return fact;
    }catch(Exception ArgumentOutOfRangeException){
    Console.WriteLine("Exception");
    }
    return 0;
    }

    static void Main(string![]! args) throws negativeException; {
    Console.WriteLine("Spec# says hello!");

    long result= findFACTORIAL(-122);
    Console.WriteLine(result);
    Console.ReadLine();
    }
    }

  • Doesn't it seem like this would make more sense using annotations or metadata for classes, as seen in the tutorial videos for Dynamic Data pages when doing custom field validation? (http://www.asp.net/learn/3.5-SP1/video-438.aspx) While a library is language agnostic, it also limits your ability to retrospectively apply contracts to any pre-existing classes without modifying the code.

  • The code written by the above person is fantastic........ Thanks buddy.

Comments have been disabled for this content.