Code Contracts Part 1 – Introduction

Series Redux

I discovered Microsoft Code Contracts several years ago and fell in love with the idea. Code Contracts have helped me to write better software since 2008 so I’d like to share them with you. I did an extensive blog series on this subject several years ago which was quite popular. However, in the years that have passed, the content got a bit stale and I’ve switched blogging platforms a couple of times. So I’m updating and offering this series once again. Please visit the series index if you would like to enjoy more articles like this one.

What is a contract?

We all have opportunities to deal with contracts now and again in our personal lives. Whether you’re leasing a car or buying a mobile phone, you’ll probably be signing a few contracts over the course of your life. But have you ever thought of the source code you write as a kind of contract? In fact, as software developers, we create contracts throughout the course each day simply by writing functions. Here’s a simple one written in C# that demonstrates the idea:

This simple method exposes a contract to which the two parties, the caller and the called function, must agree. If the Greet function could talk to its callers, it might say something like this about the contract:

Hello, my name is Greet. If you give me an array of strings, I'll give you an integer.

Because of the contract, callers can’t pass an array of integers to this function. Compilers for statically-typed languages won’t allow that. Similarly, if the Greet function tried to return something other than an integer, that would also be a violation of the contract and disallowed by the C# compiler. For the things that the C# compiler can do to enforce the agreement, we can safely call this exchange a kind of contract. However, as legally binding as this might seem, there are some lingering questions. For example:

  • Can the caller pass null (Nothing) for the args parameter?
  • Can the caller pass an empty array?
  • Can some of the strings in the array be empty or be null references?
  • Will any conversions be applied to the strings that affect valid input values?
  • Is there a limit on the length of the strings supplied?
  • How many strings can the array refer to?
  • Does the Greet function produce any noteworthy side effects in the object instance it may belong to?
  • Can the caller ignore the result of the function?
  • What range of integers can the function return to the caller?
  • Are any of the return values so-called sentinel values that have special meanings?
  • Are any exceptions potentially thrown?
  • If exceptions are thrown, are the promises about side effects still enforced? Or are there potentially different side effects when this occurs?

Well, it looks like we’re missing a few details. In a traditional, general purpose programming language like C#, the syntax doesn’t allow me to express all of the details to refine the contract more profoundly. A common approach to the ambiguities in C# might be to add some so-called guard code to the Greet function like this:

We call these kinds of defensive statements guarding because they act like a shield, keeping us from making obvious mistakes inside the function. By checking that the array isn’t null and that it contains at least one non-null element, we believe that the code in the remainder of Greet method will run cleanly. But the mechanism by which callers will be informed of their mistakes in passing bad parameters is the same. They will get exceptions at runtime which, as we know, probably won’t be handled all that well.

It would be much better to implement an exception avoidance policy instead. However, to do that, these guarding conditions need to be made known to callers before they construct their invocations. In contract language, we call these pre-conditions, meaning that they are standard terms and conditions for invoking the function correctly and that they should be pre-known because they will be applied before the body of the function runs.

Introducing Code Contracts

Microsoft Research has made available a set of tools called Code Contracts for strengthening the agreements between callers and called functions. These tools are not language specific so they work across all of the core .NET languages. In fact, if you have the .NET Framework 4.0 installed and are using Visual Studio 2010 (or a later version), you’ll find that after importing the System.Diagnostics.Contracts namespace, the following code compiles without installing any additional tools:

Pay attention to the use of the Contract class in place of the guard code I had in the last version of the Greet function shown before. The three invocations of the Requires method provide the pre-conditions that callers must meet to properly call the Greet function. The question that may be running through your mind at this point is, “If I were to violate any of those pre-conditions when calling Greet, would the compiler stop me?” The answer is no, at least not by default, which deserves a bit of explanation.

You see, the .NET 4.0 Framework includes the new namespace and the Contracts class as mentioned above, but until you install the Code Contracts for .NET tools from Visual Studio Gallery (perhaps via the Visual Studio Extensions and Updates Manager), calls to the Requires method and other members of the Contract class don’t do anything. These calls are essentially discarded during compilation if you don’t turn on the various features of Code Contracts. In this way, development computers that don’t have the Code Contracts tools installed can build and run code that includes these calls without errors. Not many research projects at Microsoft get to include optional classes in the .NET framework like. So Code Contracts must be an important piece of Microsoft’s future developer tooling plans.

After having installed the Code Contracts for .NET tools via Visual Studio's Extensions and Updates Manager.

Here’s a screenshot from my development computer after having installed the Code Contracts for .NET tools via the Visual Studio Extensions and Updates Manager. Of course, you can also download these tools directly from Visual Studio Gallery and install them yourself. No matter how you get them, you’ll probably need to restart Visual Studio after the installation if you have it open at the time.

After installing the Code Contracts tools, you’ll still not see any differences in the behavior of Visual Studio or the compilers for improper invocations of the Greet function. The pre-conditions will still seem to be doing nothing. This is by design. The Code Contract tools will be invisible until you turn specific features on. To do that, open the project properties for any project. Notice that there’s a new section (or tab) on the left side of the properties window called Code Contracts.

A new section appears in your project properties after installing the Code Contracts tools.

From the screenshot I’ve provided here, you can see that there are two major sections at the top of the Code Contracts project properties: runtime checking and static checking. I’ll show you how to use runtime Code Contracts later in this series. For now, if you’re following along by coding in Visual Studio, turn on the static checking feature, save the project settings and go back to the code.

Purple squigglies telling me that I've violated the contract.Because Code Contracts will be statically checking the code in the background, it may take some time before any indication appears that it has found some potential problems. Eventually, a squiggly purple line appears beneath a line of my code that improperly invokes the Greet method by passing null for the args parameter. In the sample I’ve shown here, I’ve positioned my mouse cursor over the line of squiggled code to reveal a message that says “CodeContracts: requires is false: args != null.” In fact, if you hovered the mouse over the previous line of squiggled code, you would see an even more ominous sounding message:

“CodeContracts: Invoking method ‘Main’ will always lead to an error. If this is wanted, consider adding Contract.Requires(false) to document it”

In other words, this program is always going to fail. That’s good to know. Of course, this was a contrived example but as we’ll see going forward in this series, Code Contracts can verify branches and assumptions across vast chains of function execution to find potential problems that you probably never realized were lurking in your software.

Ola! I have a better contract for you.

It would advisable at this point for you to stop and think about what this means for the way that you write software going forward. The basic pattern that you may have adopted for writing guard code still applies. Except now, those expressions of condition that used to be buried inside your functions can be pre-known by and visible to the callers of those functions. In the next article in this series, I’ll go deeper into the nuances of pre-conditions, showing you some of the more useful features of Code Contracts’ static verification engine.

Please visit the series index, if you would like to enjoy more articles like this one.