Sponsored By Aspose - File Format APIs for .NET

Aspose are the market leader of .NET APIs for file business formats – natively work with DOCX, XLSX, PPT, PDF, MSG, MPP, images formats and many more!

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.

This entry was posted in C#, Conferences, Spec#. Bookmark the permalink. Follow any comments here with the RSS feed for this post.
  • Greg

    @Scott Bellware

    When dealing with non-trivial invariants contracts become a much more effective model than writing unit tests as it will often require hundreds of state based tests to illustrate what can be expressed in a single contract.

    Beyond that the prover will tell you if you ever break a contract. On the TDD side you need to actually write the test in order to have the test break.

    Of course this is not 100% one way or the other. TDD and DbC are not mutually exclusive, they are complimentary. The quicker you can understand this the better off you will be. I say use BDD to show what your customer wants and to drive your development, then use contracts to handle the minutia of code as the prover will do a better job than any programming team at making sure the invariants that are defined actually are being met.

    Cheers,

    Greg

  • http://podwysocki.codebetter.com Matthew.Podwysocki

    @Liam,

    It’s very true that DbC can be used in conjunction with TDD. I do like DbC in that it makes concrete to the outside world about not only my preconditions and postconditions, but also the invariants that I maintain. That’s the tricky part to sometimes express. With DbC, that becomes part of the method signature as it were and becomes self documenting. It clears up a lot of edge cases, no doubt.

    Matt

  • http://podwysocki.codebetter.com Matthew.Podwysocki

    @Neil

    For non-null types, you would be correct, but I haven’t played with that yet, and hoping to for the next blog post coming later this week.

    Matt

  • http://podwysocki.codebetter.com Matthew.Podwysocki

    @Jim

    Thanks for the nit-pick. Always there to keep me grounded. So noted…

    Matt

  • http://www.eclipsewebsolutions.com.au Liam McLennan

    Ignoring DBC because you are doing TDD assumes that your tests are perfect. I doubt it.

  • Jim Cooper

    Nitpicking here, but min then max is easier to read:

    CodeContract.RequiresAlways(latitude >= -90.0 && latitude <= 90.0);

    and you mean “complement” not “compliment”, in your reply to Scott

  • http://neilmosafi.blogspot.com Neil Mosafi

    I thought that with Spec# the first line of your main method would have simply failed to compile?

  • http://podwysocki.codebetter.com Matthew.Podwysocki

    @Ram

    I didn’t forget to talk about it at all. It’s noted up there, especially in my posts about Spec#. I said the static verification is the most important piece. And yes, it is important to note the difference between the build styles as to whether to keep the contracts enforced or not.

    Matt

  • Ram

    You forgot to talk about the most important thing: all the contracts can be checked at compile time (static checking) !! This is far more valuable than typical runtime checking, because everything is returned as warning/errors at compile time. Furthermore, all the contracts IL is then removed when you compile in release mode, for the sake of performance, so you get the best of both worlds.

  • http://podwysocki.codebetter.com Matthew.Podwysocki

    @Sean

    That’s the thing I forgot to mention, that it is currently under the academic license. Unfortunately, until its release as part of VS2010, it will remain under that license.

    I like this approach because I can statically enforce these specs for the public APIs, and they become self documenting. That’s not to say that I still won’t do executable specs as well through BDD and such.

    Matt

  • http://kearon.blogspot.com/ sean kearon

    @Matt – this sounds very interesting indeed. The link to install into 2008 only shows a download for 2010CTP. The 2008 will be for an academic license too. Is there anything that could be used in a released application yet?

    @Scott – executable specs sounds even more interesting…any links?

  • http://podwysocki.codebetter.com Matthew.Podwysocki

    @Scott

    Does this mean you’ll be doing TDD on all third party libraries as well? That wouldn’t make sense as you assume they would work as advertised. What if you could instead, make that as part of an external contract that suddenly becomes visible to all consumers of the library. What you’re doing in TDD is something I wholly believe in and I don’t think this will ever replace that, instead compliment it. Many times, these conditions will cover the edge cases that we sometimes dread.

    Where I recommend this to be used is for public APIs, such as where it’s being used in such things as IronRuby. Self documenting API code is a good thing.

    Matt

  • http://scottic.us Scott Bellware

    Or, I could just rely on the executable specs that I’m already writing to document the software and client-drive it’s design.

    I remain unmoved. I still think this is a good approach for less mature engineering that doesn’t already understand the how, why, and what of TDD.