Code Contracts: Hiding ContractException

It’s time to move on and improve my randomizer I wrote for an example of static checking of code contracts. In this posting I will modify contracts and give some explanations about pre-conditions and post-conditions. Also I will show you how to avoid ContractExceptions and how to replace them with your own exceptions.

As a first thing let’s take a look at my randomizer.

public class Randomizer
{
    public static int GetRandomFromRange(int min, int max)
    {
        var rnd = new Random();
        return rnd.Next(min, max);
    }
 
    public static int GetRandomFromRangeContracted(int min, int max)
    {
        Contract.Requires(min < max, "Min must be less than max");
 
        var rnd = new Random();
        return rnd.Next(min, max);
    }
}

We have some problems here. We need contract for method output and we also need some better exception handling mechanism. As ContractException as type is hidden from us we have to switch from ContractException to some other Exception type that we can catch.

Adding post-condition

Pre-conditions are contracts for method’s input interface. Read it as follows: pre-conditions make sure that all conditions for method’s successful run are met. Post-conditions are contracts for output interface of method. So, post-conditions are for output arguments and return value.

My code misses the post-condition that checks return value. Return value in this case must be greater or equal to minimum value and less or equal to maximum value. To make sure that method can run only the correct value I added call to Contract.Ensures() method.

public static int GetRandomFromRangeContracted(int min, int max)
{
    Contract.Requires(min < max, "Min must be less than max");
 
    Contract.Ensures(
        Contract.Result<int>() >= min &&
        Contract.Result<int>() <= max,
        "Return value is out of range"
    );
 
    var rnd = new Random();
    return rnd.Next(min, max);
}

I think that the line I added does not need any further comments.

Avoiding ContractException for input interface

ContractException lives in hidden namespace and we cannot see it at design time. But it is common exception type for all contract exceptions that we do not switch over to some other type.

The case of Contract.Requires() method is simple: we can tell it what kind of exception we need if something goes wrong with contract it ensures.

public static int GetRandomFromRangeContracted(int min, int max)
{
    Contract.Requires<ArgumentOutOfRangeException>(
        min < max,
        "Min must be less than max"
    );
 
    Contract.Ensures(
        Contract.Result<int>() >= min &&
        Contract.Result<int>() <= max,
        "Return value is out of range"
    );
 
    var rnd = new Random();
    return rnd.Next(min, max);
}

Now, if we violate the input interface contract giving min value that is not less than max value we get ArgumentOutOfRangeException.

Avoiding ContractException for output interface

Output interface is more complex to control. We cannot give exception type there and hope that this type of exception will be thrown if something goes wrong. Instead we have to use delegate that gathers information about problem and throws the exception we expect to be thrown.

From documentation you can find the following example about the delegate I mentioned.

Contract.ContractFailed += (sender, e) =>
{
    e.SetHandled();
    e.SetUnwind(); // cause code to abort after event
    Assert.Fail(e.FailureKind.ToString() + ":" + e.DebugMessage);
};

We can use this delegate to throw the Exception. Let’s move the code to separate method too. Here is our method that uses now ContractException hiding.

public static int GetRandomFromRangeContracted(int min, int max)
{
    Contract.Requires(min < max, "Min must be less than max");
 
    Contract.Ensures(
        Contract.Result<int>() >= min &&
        Contract.Result<int>() <= max,
        "Return value is out of range"
    );
    Contract.ContractFailed += Contract_ContractFailed;
 
    var rnd = new Random();
    return rnd.Next(min, max) + 1000;
}

And here is the delegate that creates exception.

public static void Contract_ContractFailed(object sender, ContractFailedEventArgs e)
{
    e.SetHandled();
    e.SetUnwind();
 
    throw new Exception(e.FailureKind.ToString() + ":" + e.Message);
}

Basically we can do in this delegate whatever we like to do with output interface errors. We can even introduce our own contract exception type. As you can see later then ContractFailed event is very useful at unit testing.