If you haven't already done so, now would be a good time to familiarize yourself with the example in Part 1 of this series because I am going to start from that point in my discussion of how Microsoft Code Contracts pre-conditions work in this article. In the previous segment, we looked at a simple method written in C# called Greet. That method accepted an array of strings and returned an integer. Very simple stuff. We also observed that the method interface (the contract) offered by C# was fairly weak, failing to answer a whole range of questions that a caller of the Greet method might want to ask.

We saw how the static (Shared) Requires() method in Contract class could be used to add simple pre-conditions to the the Greet method. The Code Contracts static checker was used to discover some suggested pre-conditions and the reasons behind them. After the initial set of pre-conditions was written in the Greet method, another build of the solution showed us where we could add upstream pre-conditions in the Main method to satisfy the downstream assumptions. That was cool but we saw how simple Boolean tests for those conditions would also satisfy the static checker. And those bits of guard code at the call site remain effective even when the runtime checker isn't used.

Now we're ready to examine some of the alternative pre-condition capabilities in the Code Contracts toolbox. Let's go back to an earlier form of the Greet function. In this version, rather than using Contract.Requires() calls to specify pre-conditions, imagine that we've already written good legacy-style guard code in the preamble of the method like this:

public int Greet(string[] args)
{
    if (args == null)
        throw new ArgumentNullException();
    if (args.Length == 0)
        throw new ArgumentException();
    if (args[0] == null)
        throw new ArgumentException();

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

We would like to make this code compatible with Code Contracts so that callers could discover their obligations. Of course, you could go to the time and trouble of converting these three if-then-throw type expressions into Contract.Requires() calls. But if you have a lot of legacy code to get into compliance, that's a lot of work. And having the originally defined exceptions be thrown at runtime may also be a requirement. Thankfully, the smart folks on the Code Contracts team at Microsoft have recognized the investment value in the large volume of guard code that we have in our source code today. Instead of rewriting these if-then-throw pre-conditions into the Contract.Requires() form, we can place a call to Contract.EndContractBlock() after the last if-then-throw statement like this:

public int Greet(string[] args)
{
    if (args == null)
        throw new ArgumentNullException();
    if (args.Length == 0)
        throw new ArgumentException();
    if (args[0] == null)
        throw new ArgumentException();

    // this call tells the static checker and the
    // runtime rewriter that all the if-then-throw
    // statements above should be implemented as
    // discoverable pre-conditions
    Contract.EndContractBlock();

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

If you included the Main method from Part 1, building the solution with this modification should show that 22 assertions were made and all 22 were correct. Your assertion count may vary but the point to be taken here is that all of the known pre-conditions have been validated by the static checker. But how do we know that the these three legacy style pre-conditions in the if-then-throw format were interpreted as pre-conditions by Code Contracts? You see 22 assertions, no errors. How do you know?

Well, there are a couple  of ways. I'll show you both. The first way you can verify this is to look under the covers at the code that gets generated by the runtime checker. We haven't seen or used the Code Contracts runtime checker so far in this series, so let's experiment by turning it on. Go to the project properties dialog by right-clicking on the project name in the Solution Explorer and selecting the Properties... item from the context menu. On the Code Contracts tab, enable the runtime checker by checking the "Perform Runtime Contract Checking" checkbox and making sure that the mode dropdown next to it is set to Full. It should look like this:

Setting the project up to generate runtime contract checks.

Note: If you don't have a Code Contracts tab in the project properties, you probably need to install the Code Contracts add-in as described in Part 1 of this series. You can visit the Microsoft Code Contracts site and get the bits.

After enabling runtime contract checking and building the solution, open the assembly (the EXE file created by the build process) in a tool like Red Gate's Reflector or the Microsoft Disassembler (ILDASM) that ships with Visual Studio. I'm using Reflector so disassembling the Greet method and interpreting it as C# shows us this:

public int Greet(string[] args)
{
    if (__ContractsRuntime.insideContractEvaluation <= 4)
    {
        try
        {
            bool _preConditionHolds;
            __ContractsRuntime.insideContractEvaluation++;
            // compare the test on the next code line (11)
            // to the string expression used on line 21
            if (args == null)
                _preConditionHolds = false;
            else
                _preConditionHolds = true;
            if (!_preConditionHolds &&
                 (ContractHelper.RaiseContractFailedEvent(
                     ContractFailureKind.Precondition, null, 
                     // compare the string expression on the
                     // the next code line (21) to the test
                     // on line 11
                     "args != null", null) != null))
            {
                throw new ArgumentNullException();
            }
            if (args.Length == 0)
                _preConditionHolds = false;
            else
                _preConditionHolds = true;
            if (!_preConditionHolds && 
                (ContractHelper.RaiseContractFailedEvent(
                    ContractFailureKind.Precondition, null, 
                    "args.Length != 0", null) != null))
            {
                throw new ArgumentException();
            }
            if (args[0] == null)
                _preConditionHolds = false;
            else
                _preConditionHolds = true;
            if (!_preConditionHolds && 
                (ContractHelper.RaiseContractFailedEvent(
                    ContractFailureKind.Precondition, null, 
                    "args[0] != null", null) != null))
            {
                throw new ArgumentException();
            }
        }
        finally
        {
            __ContractsRuntime.insideContractEvaluation--;
        }
    }
    Console.WriteLine("Hello, {0}!", args[0]);
    return args.Length;
}

Note: If you're reading this post from a syndication source, you may not be able to see line numbers in the code listings because Alex Gorbatchev's most excellent Syntax Highlighter that I use on my blog doesn't make the trip via RSS feeds. That's too bad but you can always link back to the original version of this post if you want to see the code formatted with line numbers.

Lines 11 through 24 in the disassembly above correspond to the first if-then-throw block in the previous code listing that tests whether the args parameter is equal to null. You can clearly see the "if (args==null)" test on line 11. And you can see the corresponding ArgumentNullException being thrown on line 23. But the code in between is quite different. First of all, a Boolean variable called _preConditionHolds has been inserted and it's set to true or false depending on the outcome of the test. If the pre-condition does not hold, a call to an internal helper method called RaiseContractFailedEvent is made.

Notice on line 21 that the quoted literal string showing the pre-condition text "arg != null" is the logical opposite of the test that was performed on line 9 in the code, i.e. "arg == null". The reason for this is simple. When Code Contracts escalates a failed pre- or post-condition, it chooses to be consistent, expressing the failure to the user in terms of the condition that failed. The way we wrote the legacy-style precondition was by testing what would need to be true to throw an exception which, of course, is the logical opposite of the pre-condition test that would have failed in that case. Interesting that Code Contracts flips the legacy test around, builds a string that represents it and includes that in the RaiseContractFailedEvent call.

OK, so disassembling the code was a bit geeky. I admit that. But I find reasons to use Reflector all the time. I just love that tool and every other tool from Red Gate, by the way. An easier way to test that the EndContractBlock method actually captured our if-then-throw expressions as pre-conditions is to comment out the Contract.Requires() calls and/or the argument guard code in the Main method that we fixed in Part 1 and build the project with the static checker enabled.

static void Main(string[] args)
{
    // Let's comment out all of our pre-conditions
    // and guard code to see if the static checker
    // considers those if-then-throw style pre-
    // conditions in the Greet method real or not

    // Contract.Requires(args != null);
    // Contract.Requires(args.Length > 0);
    // Contract.Requires(args[0] != null);

    Part1 program = new Part1();
    // if (args != null && args.Length > 0 && args[0] != null)
        program.Greet(args);
}

When you do this, you will see the set of "unproven" pre-condition warnings that you might expect:

Static check shows that the if-then-throw style pre-conditions are real.

This means that the static checker really is converting our legacy style if-then-throw style guard code in the Greet method into real Code Contracts pre-conditions. In summary, using the EndContractBlock() method did two things for us:

  1. It allowed us to convert our legacy guard code into a set of pre-conditions without a lot of effort.
  2. It allowed us to preserve the throwing of specific exceptions at runtime that other legacy code may depend on. Even with the runtime checker turned on, we saw in the disassembled code that the throwing of the original exceptions are compiled in. That's valuable if you have legacy code that depends on the getting those particular exceptions.

Now, let's move on and look at another way to specify pre-conditions using Microsoft Code Contracts. In this section, we'll examine a different form of the Contract.Requires() method. Rather than describing it, try reading the code first. Hopefully the syntax is fluent enough that you can tell what this code it should be doing.

public int Greet(string[] args)
{
    Contract.Requires<ArgumentNullException>(args != null);
    Contract.Requires<ArgumentException>(args.Length > 0);
    Contract.Requires<ArgumentException>(args[0] != null);

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

My guess is that you zeroed right in on the generic <TException> syntax on the three Contract.Requires calls in this new version of the Greet method. The Contract.Requires<TException>() method is useful whenever you need to throw particular exceptions to support legacy requirements, for example. Only one rule has to be obeyed: the Exception class that's used in the generic instantiation must have a constructor that takes a single string parameter to accept the message to show to the user. That's acceptable.

If you use the Requires<TException>() pre-condition form, there's one important thing that you really need to understand. This fact that I'm going to share doesn't exactly jump out of the Code Contracts documentation. Let me illustrate the phenomenon to make it clear. Turn OFF the runtime checker in the Code Contracts project properties and build the code listed above and run it. You'll see something like this:

Weird assert when runtime checking is disabled and Reqiures<TException> type pre-conditions are used.

Now, let me say that I had to read the Code Contracts documentation over and over again to fully understand that the Requires<TException>() pre-condition form is only to be used when runtime checking is enabled. I didn't "twig on" quickly as my British friends might say. There is a comment in section 5.1.2 of the Code Contracts documentation that says "If you are using scenario 2 (Requires⟨Exn⟩) and you make your source code available to other developers, you might want to alert them that they need to use the tools to build your source." Might? I might want to alert them? I'll say! If a dialog like this popped up in a release build, my users would have no idea what do.

I suppose the good thing about the way this is implemented (I'm searching hard for an upside here) is that the actual Boolean condition being testing in the pre-condition doesn't need to fail to hold true to make the assertion dialog pop up. Anywhere you put a Requires<TException>() call, you're going to see this popup, whether the condition holds true or not. If you disassemble the code with Reflector and drill into the implementation of Requires<TException>(), you'll see something like this:

public static void Requires<TException>(bool condition)
    where TException: Exception
{
    AssertMustUseRewriter(ContractFailureKind.Precondition,
        "Requires<TException>");
}

Check out the "condition" parameter. The AssertMustUseRewriter call, which accounts for the entire body of the Requires<TException> method, doesn't even use the condition parameter. So the "args != null", "args.Length > 0" and "args[0] != null" demands in my code were ignored. Even if the generic implementation of AssertMustUseRewriter were to throw the type of exception that we wanted, it certainly has no information about the demand we made or how it was computed.

Let's follow the advice in the assertion dialog and turn on the rewriter. I'll go to the Code Contract properties for the page and turn on runtime checking at the Full level and rebuild my solution. Now when I run my little application with no parameters to make the argument array empty, and therefore invalid, I get the ArgumentException I expected. Click on the image below to see a full-sized image.

Click to see the full-sized view.

So be careful when using the Requires<TException>() form for pre-conditions. You must be certain that you intend to always build assemblies containing these types of preconditions with the runtime checker enabled. And if you pass the code to other developers, they also have to know what to do. This is somewhat unfortunate, in my opinion. When I build my code, I shouldn't have these kinds of dependencies. The code should degrade gracefully when the runtime support has been disabled. That's just my opinion.

Well that's all for this article. In the next one, we'll examine post-conditions. If pre-conditions are promises made on the way into a method call, post-conditions are promises made on the way out. And those can be very important when it comes to the assumptions that an inference engine might depend on. Until then, all the best. Enjoy!

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 as they become available.