Code Contracts: A Technique to Cut Down on Bugs

Rent, employment, house buying: you name it. If you’re an adult, chances are that you’ve signed several contracts in your life (and will probably sign many more). A contract is an agreement that defines the rights and obligations of two or more parties in order to accomplish something.

Having a proper contract in place is a powerful tool to clear doubts about what you’re allowed or not allowed to do to the apartment you live at, for instance. A contract also defines penalties for the parties that fail to fulfill their part of the agreement. If you don’t put down your house payments when they’re due, you’re pretty much guaranteed to suffer some consequences.

Contracts are everywhere in the real world. But what would it look like if we could use something similar to contracts in our code? For instance, what if we could specify “clauses” that defined the conditions required at the start and end of a function? Or maybe that specified and enforced the invariants of our objects? In this case, I’d say our programs would definitely improve in readability, safeness,?and self-documentation.

And now, what if I told you something like this already exists?

Before Code Contracts Comes Design By Contract

My first encounter with the idea of DBC (design by contract) was a few years ago, when I read the famous book Pragmatic Programmer: From Journeyman To Master?by Andy Hunt and Dave Thomas.

In the book, the authors say that the concept of DBC was first developed by?Bertrand Meyer for the language Eiffel:

[Design by contract] is a simple yet powerful technique that focuses?on documenting (and agreeing to) the rights and responsibilities of software modules to ensure program correctness.

So, in short, we can say that DBC is a technique that consists of documenting the expectations placed upon each software piece and enforcing those expectations in order to get a correct working program.

These expectations can be one of the following types: preconditions, postconditions, and class invariants. Let’s look at each of them.

Preconditions

Preconditions are nothing more than the requirements of the module to be called. (By the way, from here on, I’m abandoning the name “module.” I’ll say “method” instead, because that’s what they are, in this context.)

A method has some expectations that need to be met before it can do its job. These expectations are the preconditions. Have you ever written a guard clause to check if the argument passed wasn’t null? That’s an example of precondition.

If you think of a method as the contracted party, then the preconditions would be the rights (or demands, if you will) of the contracted party (or the obligations of the contracting party).

Postconditions

Now that we have the preconditions out of the way, it should be pretty obvious what the postconditions are: just the opposite. In other words, they’re the conditions that must be true after the method is done with its jobs. Postconditions are what’s supposed to be done after the completion of the method.

An example of postcondition is to ensure that a return string isn’t an empty string.

To continue with the real-world contract analogy, postconditions would be the obligations of the contracted party.

Invariants

Invariants are conditions that must be true to an observer external to the object, as long as that given instance lives. Internally, the invariants may not hold true at all times, but from the perspective of an external observer, they always should be.

Method Signature As Contract

Since we’re dealing with a statically-typed language, we could say that the first and most simple type of code contract at our disposal is the method signature. Take a look at the following code:

public static string Foo(int bar)
{
  // implementation
}

Here we have a static method that receives an integer as a parameter and returns a string. I’ve chosen a very generic name and didn’t even bother with an implementation since the method itself doesn’t matter to us. Its signature is what matters. And why is that, you ask? Because a method signature is a form of contract.

What if we translated the clauses of this contract to natural language? I think we’d get something like this:

• The CONTRACTING PARTY will supply an integer number.
• The CONTRACTED PARTY will deliver a character string.

It may not look like much, but think of what the compiler is doing on your behalf by enforcing these clauses. There are a potentially infinite number of ways that digital data can be interpreted. By narrowing it down to these two specific types and enforcing their usage, we’re eliminating an entire class of potential.

Mind you, the contract itself would still exist. We’d just have to enforce it by other means, such as automated tests.

Types Aren’t Always Enough

Think back to the code sample in our previous example. What if we wanted to further narrow down our range of valid inputs? Let’s say?only numbers in the range of one to 100 are to be accepted. This would equate to adding a new precondition to our contract:

• The CONTRACTING PARTY will supply an integer number.
• The integer number provided by the CONTRACTING PARTY must be greater than or equal to one and less than or equal to 100.
• The CONTRACTED PARTY will deliver a character string.

Now that we have a new precondition, how are we supposed to enforce it? Well, if you want to count on the compiler’s help, you’re out of luck here. So, what are we to do?

Designing by Contract in .NET: Enter Code Contracts

Code Contracts are an initiative from?Microsoft Research. According to its documentation, Code Contracts consist of the following components:

• Classes that you can use to mark your code, which can be found in the System.Diagnostics.Contracts?namespace.
• A static analyzer.
• A runtime analyzer.

In what ways does Code Contracts benefit you? Again, according to the docs:

The benefits of code contracts include the following:

• Improved testing: Code contracts provide static contract verification, runtime checking, and documentation generation.
• Automatic testing tools: You can use code contracts to generate more meaningful unit tests by filtering out meaningless test arguments that do not satisfy preconditions.
• Static verification: The static checker can decide whether there are any contract violations without running the program. It checks for implicit contracts, such as null dereferences and array bounds, and explicit contracts.

• Reference documentation: The documentation generator augments existing XML documentation files with contract information. There are also style sheets that can be used with?Sandcastle?so that the generated documentation pages have contract sections.

 

Getting Started With Code Contracts: a Quick Example

Consider this solution to the StringCalculator Kata:

public static int Sum(string numbers)
{
    if (numbers.Trim() == string.Empty)
        return 0;

    return numbers
        .Split(new char[] { ',' }, StringSplitOptions.RemoveEmptyEntries)
        .Select(int.Parse).Sum();
}

The following test cases pass:

[TestCase("", 0)]
[TestCase("   ", 0)]
[TestCase("1,2,3", 6)]
[TestCase("1,2,3,4,5,6,7,8,9,10", 55)]
public void Sum(string input, int expectedResult)
{
    Assert.AreEqual(expectedResult, Sum(input));
}

But now a new requirement comes in: a null string is not a valid input. How can we deal with this new contract clause by using Code Contracts? First, let’s add “using System.Diagnostics.Contracts;” to our list of usings. Then, we’ll add a new line to the “Sum” method, which makes the precondition for the method explicit.

public static int Sum(string numbers)
{
    Contract.Requires(numbers != null);

    if (numbers.Trim() == string.Empty)
        return 0;

    return numbers
        .Split(new char[] { ',' }, StringSplitOptions.RemoveEmptyEntries)
        .Select(int.Parse).Sum();
}

Just by itself, that line doesn’t do anything, though. You need to activate the Code Contracts tools in the project.

Put Contracts to Work

First, let’s go to the Visual Studio Marketplace?to download the Code Contracts installer. After downloading it, just install it the usual way.

When you’re finished installing it, right-click on the project you want to use Code Contracts with and click on “Properties.” You should see a “Code Contracts” tab in the left panel. Click on it, and you should see the following screen:

As shown in the image, select “Perform Runtime Contract Checking” and select “Full” as the type of checking to be performed. After doing that, you’re ready to save your changes and test your application.

Now, if you were to execute the “Sum” method providing null as parameter, you should get a different exception:

Get Contracts Documented

Here’s another important thing to have in mind when talking about code contracts: they’re a software artifact and, as such, should be documented.

And how would you go about that? Well, as it turns out, one of SubMain’s offerings,?GhostDoc, is the perfect tool for taking care of that documentation.

GhostDoc has a feature that consumes code contract XML tags and outputs their information in the help documentation and the Visual Editor. In order to do that, first use the Code Contracts for .NET tools to add the code contract tags to your code. Then you should be good to go!

Is That All There Is to Code Contracts?

After this very quick example, you may be thinking to yourself, “What’s the point?”? If that’s all there is to it, why not just stick to the good old duo “guard clause and throw exception”?

Well, this could be a fair point, but here’s the thing: there’s a lot more to Code Contracts than just this. As mentioned, the true power of Code Contracts lies in both the runtime and static analyses it performs, especially in regards to object invariants.

And this is just the tip of the iceberg. This post was a quick introduction to the subject, meant to leave you wanting more. Research, explore, and learn more?until you’re comfortable enough to add Code Contracts to your personal list of coding best practices.

Learn how GhostDoc can help to simplify your XML Comments, produce and maintain quality help documentation, generate documentation for Code Contracts.

About the author

Carlos Schults

Contributing Author

Carlos Schults is a .NET software developer with experience in both desktop and web development, and he?s now trying his hand at mobile. He has a passion for writing clean and concise code, and he?s interested in practices that help you improve app health, such as code review, automated testing, and continuous build. You can read more from Carlos at carlosschults.net.

This author does not have any more posts.