Should the Code Contracts static checker be able to check arithmetic bound?

by

I’ve had an answer on the MSDN forum. It turns out I was very nearly there. Basically the static checker works better if you split out “and-ed” contracts. So, if we change the code to this:

public static int RollDice(Random rng)
{
    Contract.Ensures(Contract.Result<int>() >= 2);
    Contract.Ensures(Contract.Result<int>() <= 12);

    if (rng == null)
    {
        rng = new Random();
    }
    Contract.Assert(rng != null);

    int firstRoll = rng.Next(1, 7);
    Contract.Assume(firstRoll >= 1);
    Contract.Assume(firstRoll <= 6);
    int secondRoll = rng.Next(1, 7);
    Contract.Assume(secondRoll >= 1);
    Contract.Assume(secondRoll <= 6);

    return firstRoll + secondRoll;
}

That works without any problems. It also means the example is even more useful, as it highlights the very point that the checker does work better with separated out contracts.

Leave a Comment