Должна ли статическая проверка Code Contracts проверять арифметическую привязку? - PullRequest
Новая
       28

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

34 голосов
/ 07 августа 2009

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

Ответы [ 2 ]

14 голосов
/ 08 августа 2009

У меня был ответ на форуме 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;
}

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

1 голос
/ 07 августа 2009

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

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

...