In Part 1 and Part 2 of this series, we used a very simple conversation between a pair of methods, Main and Greet, to demonstrate the basics of preconditions in Microsoft Code Contracts. In this part, we are going to switch gears and begin an examination of postconditions. And we'll use some different example code that's a bit better suited for that purpose.

If you've been reading along with this series, you already know how important it is to be able to define the obligations that function callers have. Code Contract pre-conditions allow us to document those requirements much more thoroughly than the facilities of languages like C# or Visual Basic .NET ever could. But pre-conditions really only describe one part of the conversation.

Callsite to target graphic.

In any functional conversation, there are callers and targets. From the caller's perspective, the point in the code where the call occurs is the known as the callsite. It is shown in the diagram as the point where the invocation leaves the calling method and where the results are delivered to from the target method. Our pre-conditions document the requirements at the point of invocation so that the calling method may formulate the call in a way that the target expects. When the Code Contracts runtime checker is enabled, you can think of the code for the pre-conditions being executed on the near side of the invocation arrow, i.e. at the callsite, or at the far side near the target method. Both are possible and we'll talk more about that in a future article when we discuss contract reference assemblies and the "Call-site Requires Checking" runtime option in the Code Contracts project properties page. Conceptually, for the static checker, you can associate the pre-conditions with the invocation arrow in general, not with either end of the arrow. This is because from the static checker's point of view, pre-conditions don't really execute at all. They are more like high-performance documentation.

The left-pointing arrow in the diagram, i.e. the results of the function call are, for the most part, what our post-conditions will document. At the heart of what both pre- and post-conditions document is the idea of assumptions. When a pre-condition is written that says "reference X must not be null", it's written in a way that conveys the requirement to the caller. In another way of thinking about it, from the target method's perspective, the pre-condition might read, "I assume that reference X will not be null."

In this same way, post-conditions are about being able to make assumptions. Let's look at a simple pair of methods to begin our examination of post-conditions:

using System;

public class Part3
{
    private static readonly Random _rnd =
        new Random(DateTime.Now.Millisecond);

    public int BoundedRandom()
    {
        return _rnd.Next(1, 100);
    }

    public int BoundedRandomQuotient()
    {
        return BoundedRandom() / BoundedRandom();
    }
}

The BoundedRandomQuotient method is perfectly good code that simply divides one random integer by another random integer, right? It compiles so it must be valid. But there's a potential flaw. If you turn on the Code Contracts Static checker, enable checks for "Implicit Arithmetic Obligations" and rebuild the solution the potential problem pops right out:

The Code Contracts static checker tells us where the problems are.

The two potential issues here are division by zero and overflow. But the random numbers generated by the BoundedRandom method will always be between and including 1 to 100 meaning that the integer quotient will always be between and including 0 to 100. But the static checker doesn't know that. So the code as it stands right now is technically OK. We could choose to instruct the contract checker to be quiet about the quotient method by adding an special attribute to the BoundedRandomQuotient like this:

[ContractVerification(false)]
public int BoundedRandomQuotient()
{
    return BoundedRandom() / BoundedRandom();
}

After adding the [ContractVerification( false )] attribute to the BoundedRandomQuotient method and rebuilding, you'll see that the warnings go away. The ContractVerification attribute can be used to enable or disable the static checker and the output of the rewriter for runtime checking at the method, class or assembly levels. It's a very handy way to reduce the noise when you're refactoring a large legacy code base with Code Contracts, in fact, typically by turning verification off for whole assemblies at first, then narrowing down to specific classes, then down to specific methods. But in this particular case, turning off verification on the BoundedRandomQuotient method was not the correct choice for dealing with the warnings from the static checker. Imagine that at some point after turning off the verification, the BoundedRandom method is modified to read:

public int BoundedRandom()
{
    return _rnd.Next(0, 100);
}

Notice the simple change? Now, the BoundedRandom method can return 0 so BoundedRandomQuotient could end in an ugly DivideByZeroException type result. But a rebuild of the project with the Code Contracts static checker turned on shows no potential problems because of the [ContractVerification( false )] attribute that we applied to the BoundedRandomQuotient method to silence it earlier. Kevin's advice: never use the ContractVerification attribute to disable Code Contracts checkers unless you have no other option. It's perfectly OK to use the ContractVerification attributes to reduce noise when you're refactoring but be sure to remove them all when you're done.

Let's go back and handle the problem in the original code the correct way by adding a post-condition:

public int BoundedRandom()
{
    Contract.Ensures(Contract.Result<int>() >= 1);
    return _rnd.Next(1, 100);
}

Just as the Contract.Requires static method can be used to specify pre-conditions, you can see that the Contract.Ensures method can be used to document post-conditions that must hold true when the method returns. Notice that another generic method, Contract.Result<TResult>, is used inside the Ensures statement to describe the post-condition in terms of the method's resulting value. The Contract.Result<TResult> method is very special in that it may only be invoked inside an Ensures statement. In this code, it gives us a way to refer to the unnamed integer result of the BoundedRandom method. And because it's generic, we must specify the correct result type for the method in the type parameter, in this case an integer. In the voice of the BoundedRandom method speaking to its potential callers, the Ensures statement essentially says, "You may assume that the result of this function will always be greater than or equal to one." Removing the [ContractVerification( false )] attribute from the BoundedRandomQuotient method and rebuilding shows that the original warnings emitted by the static checker are now gone. Moreover, they are gone for the right reason, not that we ignored a potential problem but that we documented what the BoundedRandom method guarantees. The BoundedRandomQuotient method can now factor that guarantee, that promise, into the assumptions it makes about its own work.

Now that the post-condition is in place, let's go back and make the change that started our trouble a few minutes ago:

public int BoundedRandom()
{
    Contract.Ensures(Contract.Result<int>() >= 1);
    return _rnd.Next(0, 100);
}

After changing the Next method call on the random number generator to potentially produce zeroes in the output again, what do you think the static checker will say when we rebuild? Well, if you guessed that it will generate a warning, you are correct. The error output window now looks like this:

Build warnings after violating a post-condition.

What's interesting here is that the Code Contracts static checker knows something about how the Random::Next(lowerBound, upperBound) method works. It seems to know that the results are indeed bounded by the lowerBound and upperBound parameters. And by changing the lowerBound parameter to zero, we cannot prove that the result of the BoundedRandom function will be greater than or equal to one as the contract states. That gives us a very nice feeling knowing that the tools are backing us up and preventing future breaking changes. With the proper post-conditions in place, an inexperienced or careless programmer can't ramble through the code making changes that could violate the contract without changing the contract itself.

In general, I believe that the right to modify code contracts should be reserved for senior developers and those others who know the business rules driving the system. Or, at a minimum, any changes to Contract.Requires and Contract.Ensures statements must undergo a peer review process. Changing code is like changing data in the database realm. But changing a code contract is like changing the metadata or schema of a database. In my opinion, those kinds of changes should be subject to a much more rigorous and demanding review process.

In closing, I'll finish this article by talking about the placement of the Contract.Ensures calls in your code. You may be tempted to place your post-conditions at the end of your methods. This makes sense because the results of a method are typically calculated nearer the bottom of most methods. And we see what looks like real code when we read a well-formed C# statement invoking the static Contract.Ensures method. So we naturally think that the call must be placed in context to return the value of some local variable which holds the result, probably nearer the bottom of the method. But unless the rewriter for the runtime checker is turned on, there's no code emitted for calls to Contract.Requires or Contract.Ensures. Remember, these invocations really serve as markers for documentation or metadata that the static checker and the rewriter can use. So it's important to group all of those bits of the contract at the top of the method call. In fact, there's a strict requirement to do this.

The end of the contract block is sensed by Code Contracts when the first non-contract call is encountered, reading top to bottom, or when a call to Contract.EndContractBlock() is encountered. We examined the EndContractBlock method briefly in Part 2 of this series when we looked at legacy style if-then-throw pre-conditions. The EndContractBlock was used there to signal to Code Contracts that the if-then-throw code found in the preamble of the method should be interpreted as a set of pre-conditions. However, the EndContractBlock call can be used in any method to signal the end of the code contract whether they use if-then-throw style pre-conditions or not. Personally, I like using an EndContractBlock call in all my methods that specify Code Contracts because it makes the code very readable. It tells a good story to read about all of the requirements metadata and documentation that the contract will produce followed by the clarity and finality of a statement that says, "The contract ends here." I just like that. Whether you use the EndContractBlock calls in methods that don't require it is up to you. It's really a matter of style.

That's all for now. We'll dig deeper into post-conditions in the following articles in this series. Hopefully, though, this piece has given you the basics that you'll need to progress from here. 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.