Кодовые контракты - Предположим против требований

Ответ 1

Представьте, что у вас есть такой способ:

bool ContainsAnX(string s)
{
    return s.Contains("X");
}

Теперь этот метод всегда будет терпеть неудачу, если вы передадите ему null, чтобы вы этого не делали. Для этого используется Contract.Requires. Он устанавливает предварительное условие для метода, который должен быть истинным для правильного запуска метода. В этом случае мы имели бы:

bool ContainsAnX(string s)
{
    Contract.Requires(s != null);

    return s.Contains("X");
}   

( Примечание: Requires и Ensures всегда должно быть в начале метода, так как это информация о методе в целом. Assume используется в самом коде, так как это информация об этой точке в коде.)

Теперь, в вашем коде, который вызывает метод ContainsAnX, вы должны убедиться, что строка не равна null. Ваш метод может выглядеть так:

void DoSomething()
{
    var example = "hello world";

    if (ContainsAnX(example))
        Console.WriteLine("The string contains an 'X'.");
    else
        Console.WriteLine("The string does not contain an 'X'.");
}

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

Однако вы можете обращаться к внешним библиотекам, у которых нет информации о возвращаемых значениях (т.е. они не используют кодовые контракты). Изменим пример:

void DoSomething()
{
    var example = OtherLibrary.FetchString();

    if (ContainsAnX(example))
        Console.WriteLine("The string contains an 'X'.");
    else
        Console.WriteLine("The string does not contain an 'X'.");
}

Если OtherLibrary не использует Code Contracts, статический контролер будет жаловаться, что example может быть нулевым.

Возможно, их документация для библиотеки говорит, что метод никогда не вернет null (или никогда не должен!). В этом случае мы знаем больше, чем статическая проверка, поэтому мы можем сказать ей Assume, что переменная никогда не будет равна null:

void DoSomething()
{
    var example = OtherLibrary.FetchString();

    Contract.Assume(example != null);

    if (ContainsAnX(example))
        Console.WriteLine("The string contains an 'X'.");
    else
        Console.WriteLine("The string does not contain an 'X'.");
}

Теперь это будет в порядке со статическим контролером. Если вы включили контракты времени выполнения, то в течение времени выполнения будет также проверено значение "Предположим".

Другой случай, когда вам может понадобиться. Предположим, что ваши предварительные условия очень сложны, и статический контролер испытывает трудности с их проверкой. В этом случае вы можете немного подтолкнуть его:)

С точки зрения поведения во время выполнения не будет большой разницы между использованием Assume и Requires. Однако результаты со статической проверкой будут сильно отличаться. Смысл каждого также различен, с точки зрения того, кто несет ответственность за ошибку в случае сбоя:

• Требуется означает, что код, вызывающий этот метод, должен гарантировать, что условие выполнено.
• Предположим, что этот метод делает предположение, которое должно всегда считаться истинным.

Ответ 2

Он отличается только временем времени разработки/статического анализа

Contract.Assume: "Направляет инструменты анализа кода, чтобы предположить, что указанное условие истинно, даже если оно не может быть статически доказано, что оно всегда истинно" А также: Во время выполнения этот метод эквивалентен использованию метода Assert (Boolean).

Contract.Requires гарантирует, что данный предикат является истинным, а анализаторы статического кода могут вызвать ошибку, если они не могут "доказать", что это не так. On Contract.Assume статический анализатор будет продолжать/выдавать предупреждение/независимо от того, что инструмент решит.

Ответ 3

Согласно официальная документация: страницы 7 (предварительные условия) и 11 (предполагается).

Требуется:

• Является предварительным условием ( "предварительные условия подкрепляются с помощью Contract.Requires" );
• В качестве предварительного условия будет выполняться метод invoke;

Предполагает:

• Не предварительное условие, а не постусловие, а не инвариант;
• Выполняется в том месте, где оно указано;
• стр. 11 "Существуйте в сборке только в том случае, если определен символ полного контракта или символ DEBUG";