This blog post is part of a series concerning Microsoft Code Contracts. For a complete series directory, please refer to the following list. Articles without a link will be published soon.

  • Part 01 - Introduction
  • Part 02 - Preconditions & Postconditions
  • Part 03 - Runtime Support
  • Part 04 - Abstract Types and Interfaces
  • Part 05 - Global Postconditions
  • Part 06 - Assert, Assume, ForAll and Exists
  • Part 07 - Contract and Invariant Inheritance
  • Part 08 - Contract Reference Assemblies
  • Part 09 - Refactoring a Legacy Code Base
  • Part 10 - Writing a Custom Contract Runtime Class
  • Part 11 - Documenting Code Contracts
  • Part 12 - Command Line Tools
  • Part 13 - Contracts in Continuous Integration
  • Part 14 - A Chat with Microsoft's Code Contracts Team

Microsoft Code Contracts have finally emerged from the Microsoft Research DevLabs into production. This is the first in a new blog series dedicated to spreading the good news about this amazing product. You may already know that Microsoft dumps billions of dollars into Research & Development every year, collaborating with academic, government and industry researchers all over the world to improve the platform. To be frank, this "culture of investment" is the main reason that I'm proud to call myself a .NET developer. Microsoft's deep level of investment is also attracting some of the best and brightest minds in software engineering to their research projects: another great reason for me to reply in kind, dedicating myself to mastering the platform.

Along the journey to becoming a Microsoft ninja, I discovered Code Contracts in 2008 and immediately fell in love with the idea. Code Contracts is just one of the many DevLabs projects that are part of the RiSE program, or Research in Software Engineering at Microsoft. Among its cryptic-sounding project peers like CHESS, Doloto, Pex, Moles, Cuzz, Gargoyle, etc., the Code Contracts project has a name we can actually ascribe some purpose to. We all know what code is and we certainly have opportunities to deal with contracts now and again. In fact, as software developers, we deal with code contracts (lowercase) every day. Here's an example:

public int Greet(string[] args)
{
 Console.WriteLine("Hello, {0}!", args[0]);
 return args.Length;
}

This simple Greet method written in C# exposes a contract. If it could talk, the Greet method might say:

  • I promise to accept an array of arguments of type string.
  • I promise to return an integer type result when I am done.

These promises can be thought of as contractual obligations. The Greet function is obligated to to fulfill the promises it has made. Similarly, callers of the Greet function have some obligations, too. You can't just pass an array of integers as arguments. The contract requires an array of strings. And if the caller tried to handle the integer result of the Greet method as a string, for example, that would be a violation of the contract, too. So, the simple interface of this little method creates obligations both for the caller and within the implementation of the Greet method. I think we can safely call this exchange of obligations a contract, enforceable and verifiable in every legal sense of the term. However, as legally binding as this contract "language" might be, there are some unanswered questions:

  • Can the caller pass null (Nothing) for the argument?
  • Can the caller pass a valid but empty array of strings as the argument?
  • How many strings in the arguments array does the Greet method expect?
  • Can the caller safely pass non-null but empty strings as arguments?
  • Arrays are reference types, so Greet could replace some or all of the string references in the arguments passed to it. Does it intend to do that?
  • Does the Greet method modify the state of the object of which it's a part?
  • Does it have any other side effects that the caller needs to know about?
  • Can the caller ignore the integer result of Greet?
  • What range of integers does Greet intend to return?

Wow! It looks like the attorneys who wrote our little code contract left out some important details, you might say. (No offense to Hejlsberg, Stroustrup, Kernighan or Ritchie, of course.) There are a lot of loopholes in this contract it seems. In a traditional, general purpose programming language like C#, we might add some "guard code" to the Greet method to tighten things up a bit like this:

public int Greet(string[] args)
{
 if (args == null)
 throw new ArgumentNullException();
 if (args.Length  1 || args[0] == null)
 throw new ArgumentException();
 
 Console.WriteLine("Hello, {0}!", args[0]);
 return args.Length;
}

We call the kinds of defensive statements at the top of this revision "guard code" because they act like a shield, keeping us from making obvious mistakes later in the method. By checking that the array isn't null and that it's at least one element in length and that the first element is also not null, we believe that the code in the remainder of Greet method will run smoothly or at least without exception. These tests will allow us to check that the array passed to Greet is structured and populated just as we require. You might even call the assumptions at the top of the function a set of "code-conditions" that must be met to execute the Greet method correctly.

These new code-conditions are good but they're not really acting like code-conditions at all. C# gives us no way of describing them to callers of the Greet method. Looking at the Greet method signature alone, callers have no way of knowing what their non-null and array bounds obligations are. Microsoft Code Contracts doesn't see this as a deficiency in the C# language at all. Sure, languages like Eiffel have the ability to express pre-conditions in code but C# and VB.NET weren't created to be design-by-contract languages. The approach that Microsoft took with Code Contracts is very simple:

  1. Let the .NET languages be what they want to be.
  2. Provide some scaffolding above the code (through a static checker).
  3. Provide a safety net below the code (through a runtime rewriter).

I'll spend the rest of this post talking about the static checker and focus on the Code Contracts runtime rewriter in future posts. The Code Contracts static checker is only available in the Premium Edition of the product which, in turn, only functions on Visual Studion 2008 Team System and the Premium or Ultimate Editions of Visual Studio 2010. Once you have Code Contracts Premium Edition installed, the static checker is enabled by checking a checkbox on a new "Code Contracts" tab in the project properties.

In this new tab marked "Code Contracts", notice that I've selected four checkboxes from the middle section entitled Static Checking:

  • Perform Static Contract Checking
  • Implicit Non-Null Obligations
  • Implicit Array Bounds Obligations
  • Check in Background

Perform Static Contract Checking means that I want to enable the static checker. Remember that if you are running the non-Team System version of Visual Studio 2008 or the Standard Edition of Visual Studio 2010, you will not have access to the static checker. Later posts in this series will cover the runtime Code Contracts checker which all versions of Visual Studio have access to. Checking this checkbox enables the feature in general and you'll notice that if you uncheck it, the rest of the options in that section become visually disabled.

Implicit Non-Null Obligations means that we want the static checker to look for places in the code that seem to implicitly obligate callers to pass a non-null reference, for example. When these kinds of pre-conditions are found, the static checker will make recommendations about adding some requirements to the contract.

Implicit Array Bounds Obligations means that the static checker should look at how arrays are used and to make some recommendations about which preconditions should be added to the contract.

Check in Background is self-explanatory, I think.

Going back to the original version of the Greet method above, let's build the solution (Ctrl+Shift+B) and see what the static Code Contracts checker has to say in the Errors List. Press Ctrl+W, E meaning "show the Window for Errors" if it doesn't show for you automatically.

There are two warnings about the args array: one that says we should check the parameter for nullness and another that says we should make sure that the length of the array is greater than zero. Great suggestions. But notice how the informational messages above the warnings encourage us to do this. They say that we should add preconditions using some method called Contract.Requires(). We are already accustomed to adding guard code using the "if (condition) throw new Exception();" pattern, right? What is this Contract.Requires() method anyway?

As you might have guessed, Microsoft Code Contracts provides the static (Shared in VB.NET) Requires() method on the Contract class in the System.Diagnostics.Contracts namespace for adding preconditions to a contract. If we follow the suggestions, adding one more pre-conditions of our own, the code including the Main function to call Greet would look like this:

using System;
using System.Diagnostics.Contracts;
 
class Part1
{
 static void Main(string[] args)
 {
 Part1 program = new Part1();
 program.Greet(args);
 }
 
 public int Greet(string[] args)
 {
 Contract.Requires(args != null);
 Contract.Requires(args.Length > 0);
 Contract.Requires(args[0] != null);
 
 Console.WriteLine("Hello, {0}!", args[0]);
 return args.Length;
 }
}

At this point, you're probably saying something to yourself like, "Well, that's a bit easier to read but how is it any better than testing with an if statement and throwing an exception for each bad condition encountered? The answer comes when you build the solution again and look at what the static checker has to say about the new code:

Now we've got a whole new batch of warnings. How is this better?! Well, let's look at each one. We'll start with the warning marked as number 2:

  • 2 CodeContracts: requires unproven: args[0] != null
    If you double-click on this warning, it opens the editor and takes the cursor to line 9, inside the Main method. Huh? How could adding a pre-condition to the Greet method create a warning in the Main method? Unless the static checker is telling us that there's now something potentially wrong with the call to Greet on that line. Indeed, if you look at the warning closely, it says that the requirement is "unproven". What does that mean? Well, if you go back and think about the original argument I made concerning the contractual nature of code, the requirements that a method makes on the caller are often expressed in simple "if (condition) throw new Exception();" syntax inside the called code. In the past, we've had no way of making the caller of a method containing such guard code to (a) know what all the obligations in calling the method are and (b) have an opportunity to express them in a way that can verify the correctness of the implementation. With the static checker in Code Contracts, it appears that we're getting just that kind of information for the first time. The static checker, if it could talk, would be saying, "You've said that the Greet method requires certain things about its parameters, but the Main method hasn't convinced me that it's actually holding up its end of the contract." Stop for a moment and savor this. This is new and different and way cool.
  • 3 + location related to previous warning
    If you double click on this warning, it will take you to the place in the Greeting method where the "args[0] != null" pre-condition was expressed. It's telling us that a specific pre-condition caused the warning above. That's a nice feature for tying warnings to the assertions and pre-conditions that created them.
  • 4 CodeContracts: requires unproven: args.Length > 0
    Like the warning on line 2, this warning is telling us that a pre-condition stated in the Greet function is also not being met in the call to Greet within Main on line 9 of the source code. The code in Main doesn't know that the args array has elements in it so the call to Greet might occur using an invalid value.
  • 5 + location related to previous warning
    Like the warning on line 3, this one says that warning 4 is related to a specific pre-condition in the Greeting method, namely the one that the length of the args array be greater than zero. Double-clicking the warning will take you directly to that pre-condition.

Looking at the suggestion on Line 1 in the Errors List, we could add some Contract.Requires() style pre-conditions to the Main function like this:

static void Main(string[] args)
{
 Contract.Requires(args != null);
 Contract.Requires(args.Length > 0);
 Contract.Requires(args[0] != null);
 
 Part1 program = new Part1();
 program.Greet(args);
}

And a build of the solution with those changes to Main would show you that all of the Code Contracts assertions had been met without warning. Excellent! But what if the Code Contracts runtime checker hasn't been enabled? Couldn't you still call the Main method of the program without command line arguments, making the args parameter an empty array? Sure you could! So, in my opinion, the following change to Main is even better:

static void Main(string[] args)
{
 Part1 program = new Part1();
 
 // testing the args parameter is enough to
 // satisfy the static checker that we won't
 // call the Greet method with bad parameters
 if (args != null && args.Length > 0 && args[0] != null)
 program.Greet(args);
}

You can leave the Contract.Requires() pre-conditions in the Main method if you like. That would be a good thing to have if the runtime checker is enabled at build time. But if you build this latest version of Main into the project, you'll see that those pre-conditions are not strictly required. The static checker simply wants to know that the pre-conditions in the Greet method have been met. And that can be done by asserting the pre-conditions upstream to the caller of Main. Or, as the code here shows, simply testing the args parameter and avoiding calls to the Greet method when the parameter is invalid will have the same effect on the static checker. Build this code and see that all the assertions have been met, satisfying the static checker that this code is both correct and safe.

Well, that's it for this post. In closing, let me tell you that if you are targeting the 4.0 .NET Framework, you don't need to add any assembly references for the code shown here to work. The Code Contracts classes are part of the 4.0 Framework. However, if you want to target the 3.5 Framework instead, you'll need to find the Microsoft.Contracts assembly in the Global Assembly Cache (GAC) and reference it to make this code build. In the next post in this series, we'll look at some interesting alternatives for specifying pre-conditions.