Должна ли статическая проверка контрактов кода иметь возможность проверять арифметическую привязку?

Question

(Также опубликовано на форуме 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].

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

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

РЕДАКТИРОВАТЬ:Теперь я обнаружил, что в статической проверке есть очень сложные варианты арифметики.Используя «расширенное» текстовое поле, я могу опробовать их в Visual Studio, но, насколько я могу судить, нет достойного объяснения того, что они делают.

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

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

Answer 2

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

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