Должен ли статический контролер 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, но, насколько я могу судить, нет достойного объяснения того, что они делают.

Ответ 1

У меня был ответ на форуме MSDN. Оказывается, я был почти там. В основном статичная проверка работает лучше, если вы разделите "и-ed" контракты. Итак, если мы изменим код на это:

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

Это работает без проблем. Это также означает, что пример еще более полезен, поскольку он подчеркивает тот факт, что контролер работает лучше с выделенными контрактами.

Ответ 2

Я не знаю о инструменте MS Contracts Checker, но анализ диапазона - это стандартный метод статического анализа; он широко используется в коммерческих инструментах статического анализа для проверки законности выражений в индексе.

MS Research имеет хороший послужной список при таком статическом анализе, поэтому я ожидаю, что такой анализ диапазона станет целью Checks Checker, даже если он не проверен в настоящее время.