Должен ли статический контролер Code Contracts проверять арифметические ограничения?

(Также размещен на форуме MSDN - но это не так много трафика, насколько я могу видеть.)

Я пытаюсь привести пример Assert и Assume. Вот код, который у меня есть:

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;
}

(Дело в том, что возможность передачи в нулевой ссылке вместо существующей ссылки Random является, конечно, чисто педагогической.)

Я надеялся, что если контролер знал, что firstRoll и secondRoll были в диапазоне [1, 6], он мог бы решить, что сумма находилась в диапазоне [2, 12].

Это необоснованная надежда? Я понимаю, что это сложный бизнес, который точно определяет, что может произойти... но я надеялся, что контролер будет достаточно умным:)

Если это не поддерживается сейчас, знает ли кто-нибудь, может ли он быть поддержан в ближайшем будущем?

EDIT: теперь я обнаружил, что в статическом контроле есть очень сложные варианты арифметики. Пользуясь "расширенным" текстовым полем, я могу попробовать их из Visual Studio, но, насколько я могу судить, нет достойного объяснения того, что они делают.

Ответы

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;
}