Design by Contract with .NET 4.0

Author: Fredrik Kalseth

An entry about visual studio | .net 4.0 Publication date 6. November 2008 16:33

Justin van Patten has put together a great list of all the new features that will ship with .NET 4.0 – both new features in the BCL, as well as the new features in the C# language itself. One of the additions to the BCL comes from Microsoft Research, and is called Code Contracts.

Code Contracts is a language independent tool which allows you to embed rules about the inputs, outputs and invariants in your code. When this information is embedded in the code, the Code Contract tools can perform both static and runtime analysis of the code to ensure that it is not breaking any of the rules defined. Sounds a lot like Spec#, doesn’t it? Well, Code Contracts is essentially a port of the static and runtime verification concepts from Spec# into an API which will ship as part of the .NET 4.0 Base Class library.

Let´s look at an example: Imagine that we have an API with the following silly method somewhere in it:

public static string GetTypeName(object obj)

{

if(null == obj) throw new ArgumentNullException(«obj»);

return obj.GetType().Name;

}

The problem with this, is that there´s no way for a client of this API to know what happens if they pass a null value to this method. Does it crash? Return a null? Return an empty string? By using the Code Contract API, we can make such details of our implementation explicit:

public static string GetTypeName(object obj)

{

CodeContract.Requires(null != obj);

return obj.GetType().Name;

}

If someone writes code that calls this method and passes a value that might be null, and we have static checking of code contracts turned on in our project, we will get the following warnings from the compiler:

The first warning tells us that the contract we have defined was violated (not very helpful the messages yet, but it is an early beta after all), and the second warning points us at the code that is violating the contract.

In addition to setting up contracts that constrain the inputs to a method, we can also set up contracts that talk about the outputs. for instance, imagine that our original method looked like this instead:

public static string GetTypeName(object obj)

{

return null != obj ? obj.GetType().Name : «<null>»;

}

This time, our method will happily accept an argument which is null, and it will always return a string. Using code contracts, we can embed this fact into our method:

public static string GetTypeName(object obj)

{

CodeContract.Ensures(CodeContract.Result<string>() != null);

return null != obj ? obj.GetType().Name : «<null>»;

}

These examples are just scratching the surface of what is possible. In addition to defining contracts that talk about the entry and exit points of methods, there´s also invariant contracts that deal with the state of the object as a whole. Contracts can also be defined on interfaces. More tools that take advantage of the contracts will also become available – for instance tools that auto-generate documentation, and of course there are great opportunities for integration with PEX here.

If you want to learn more about the features available and how they all actually work under the covers, then check out the recording of the PDC 2008 session by Mike Barnett and Nikolai Tilmann over at Channel9. I really recommend watching it – they do a great job of explaining the concepts (the first part is about Code Contracts, the second about PEX).

You can also go and download a preview of the framework and tools for Visual Studio 2008 over at the Microsoft Research site.

Comments

11/9/2008 7:28:51 PM

Interesting concept. One thing that I like in Java is the syntax

void SomeMethod(object i) throws MyNullArgumentException {…}

..as it makes the expectations of the function more explicit.

But this is just an excuse to make you a silly question: why do you write «null==obj» instead of «obj==null»? Any specific reason, or just a question of style?

Keep up your great blog, lots of good information here.

Lerxst

11/10/2008 10:26:28 AM

Thanks, glad you like it!

I agree that the checked exceptions in Java are useful, however they can also be quite annoying, so overall I think I’m glad we don’t have them in C#. With Code Contracts you can introduce a CodeContract.Throws contract to define an exceptional postcondition.

I picked up the null == obj style from a code design guideline I had to follow a while back, and it has just stuck with me ever since.. just out of habit I guess

Fredrik

2/17/2009 11:28:02 PM

I was never a big C++ coder, but I think the whole null==obj thing allowed for shortcutting or some perf gain in C++. Does not apply in Java or CLR languages from what I understand. I personally think it makes the code less readable, but that’s just me.

Nice blog.

Don Smith