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

Question

(Also posted on the MSDN forum - but that doesn't get much traffic, as far as I can see.)

I've been trying to provide an example of Assert and Assume. Here's the code I've got:

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

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

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

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

    return firstRoll + secondRoll;
}

(The business about being able to pass in a null reference instead of an existing Random reference is purely pedagogical, of course.)

I had hoped that if the checker knew that firstRoll and second roll were each in the range [1, 6], it would be able to work out that the sum was in the range [2, 12].

Is this an unreasonable hope? I realise it's a tricky business, working out exactly what might happen... but I was hoping the checker would be smart enough :)

If this isn't supported now, does anyone here know if it's likely to be supported in the near-ish future?

EDIT: I've now found that there are very complicated options for arithmetic in the static checker. Using the "advanced" text box I can try them out from Visual Studio, but there's no decent explanation of what they do, as far as I can tell.

Answer 1

I don't know about the MS Contracts Checker tool, but range analysis is a standard static analysis technique; it is widely used in commercial static analysis tools to verify that subscript expressions are legal.

MS Research has a good track record at this kind of static analysis, and so I'd expect doing such range analysis to be a goal of the Contracts Checker, even if not presently checked.

Answer 2

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.