Using Code Contracts for Safer Code

Note: This was presented to the Tampa C# Meetup on April 20th, 2011.

One of the greatest challenges in writing code is that nebulous time when the code is too complex to keep the flow all in your head, and when the debugger gets too much in the way for watching the state of your program as it runs. This is the coding twilight zone in which the quality of the code tends to drop as you add line after line of instrumentation to your code to find that spot where something goes wrong. For most of my code writing career I solved this by littering my code with lines like the following:

10 PRINT "Value= A$
printf("Value=%s\n”, pszTemp);

std::cout << "Value = " << sTemp << std::endl;
Console.WriteLine("Value={0}", temp);

and finally

log.Debug(() => "Value = " + temp);

When I finally found the problem, I would try and unwind all the tracing that I no longer need, and I would harden the lines that I think would be useful to keep long term. Sometimes, the logging would not be enough, and I would add some test logic, or assertions to try and catch some erroneous condition. The approach was sometimes haphazard or when as I worried more about maintenance, it solidified into some proper coding guidelines. Either way, it was not much more than tracing and loads of parameter tracking entering most methods. The problem was that the language or the compiler did not offer much built in support or help.

Even when I invested the time to truly harden the code by checking every value going into a method, every property changed, and the values returned, I would often skimp on the documentation. It was just too time consuming.

Sometime ago, one of the teams at Microsoft decided to address this problem. To that end, Microsoft added support for code contracts into .NET 4. Enough history, lets get to it.

Features

Ok, I lied. Before we get to it, here are the main features you should be aware of.

Runtime Checking

The binary rewriter does just want its name says. It rewrites the compiled code to embed your contracts. This is more than just implementation of the library code you added. This is similar to the runtime stack checking, or bounds checking, or overflow checking that the compiler already does. This gives the developer the ability to add custom runtime checks similar to modifying the virtual machine to support them.

Static Checking

Static checking allows the compiler to verify your code and report errors or warnings directly in Visual Studio.

Documentation Generation

Often overlooked, this is what I consider to be one of the best features. The ability to document your code requirements is very powerful, and the Code Contracts system will modify your standard .NET generated XML documentation with your contracts. Users of your code will actually know what to expect.

Installation

Code Contracts is a combination of a class library and code modification tool. The class library is part of .NET 4, but if you are using .NET 3.5, Visual Studio 2008, or want the runtime checking, you will need to install the DevLabs: Code Contracts.

Here is the description from the web site.

Code Contracts comes in two editions: * Code Contracts Standard Edition: This version installs if you have any edition of Visual Studio other than the Express Edition. It includes the stand-alone contract library, the binary rewriter (for runtime checking), the reference assembly generator, and a set of reference assemblies for the .NET Framework. * Code Contracts Premium Edition: This version installs only if you have one of the following: Visual Studio 2008 Team System, Visual Studio 2010 Premium Edition, or Visual Studio 2010 Ultimate Edition. It includes the static checker in addition to all of the features in the Code Contracts Standard Edition.

Decide which you need, and download it – either Standard Edition or Premium Edition.

{: .float_right }Configuring Your Project

After you install Code Contracts, you will be able to enable runtime and static checking using the Code Contracts tab under the project settings.

Assertions

Assertions are what most people think of when they start using code contracts, and there is no real surprise here – it is supported. There are a lot of options, but for now, just check Perform Runtime Contract Checking, and check Perform Static Contract Checking. This will enable everything needed for the samples in this post. You can read about the other options on the Code Contracts web site, or in the documentation.

For this example, we are going to simulate a hypothetical bank. As in real life, our bank should follow a number of rules. Here are the very simple rules we are require.

  1. All deposits must be a value greater than $0.00.
  2. The current balance of any bank account must be $0.00 or greater.
  3. No withdrawal can be greater than the current balance.
  4. Retrieving the current balance must not change the state of the account.

The Starting Class

This first version offers no protection and is most definitely not a place to bank. Here is the test program.

In our test case, we perform all manner of bad behaviors, and our bank class accepts them all.

Addition of Assertions

This first modifications adds a contract check at the beginning of each method. First, the Deposit method verifies that the deposit is greater $0.00. Second, the Withdrawal method verifies that the value is not greater than the current balance and is not equal or below $0.00. Our bank is safer, but still not great.

Ensures

This bank builds upon the sample with assertions, and adds an ensures check in both the Deposit and Withdrawal that ensures that the CurrentBalance is equal or greater than $0.00. This simple check makes sure that the method exists in a known and valid state.

Invariants

This final class removes the ensures and replaces it with a single invariant method. Why do this? This allows for a single set of rules to verify the state of the class is valid, no matter which method is called. I do not need to remember to add the ensures in each method. Instead, I would use ensures for specific verification that is unique to the method.

And So Much More

This is just a short introduction to the Code Contracts available for .NET. There is a lot more to contracts, but just these three concepts will be enough to make your code significantly safer, more maintainable, and overall better for your users.

Related

comments powered by Disqus