Как работает Contract.Ensures?

Я начинаю использовать кодовые контракты, а Contract.Requires - довольно прямолинейно, у меня возникают проблемы с тем, что действительно делает на самом деле.

Я пробовал создать простой способ:

static void Main()
{
    DoSomething();
}

private static void DoSomething() 
{
    Contract.Ensures(false, "wrong");
    Console.WriteLine("Something");
}

Я никогда не вижу сообщение "неправильным", но не бросает исключения или что-то еще.

Итак, что он на самом деле делает?

Ответы

Ответ 1

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

Заблуждение о Contract.Ensures заключается в том, что вы пишете его в начале метода, но оно выполняется в конце метода. Переписывающий делает все волшебство, чтобы убедиться, что он выполняется надлежащим образом, и при необходимости получает возвращаемое значение.

Как и многие вещи, касающиеся Code Contracts, я считаю, что лучше всего запустить Reflector по результатам инструмента перезаписи. Удостоверьтесь, что у вас есть настройки правильно, а затем выясните, что сделал переписывающий.

EDIT: Я понимаю, что еще не выразил точку Contact.Ensures. Проще говоря, чтобы убедиться, что ваш метод сделал что-то к концу - например, он мог убедиться, что он добавил что-то в список или (что более вероятно), что возвращаемое значение не является нулевым, или положительным, или что-то еще. Например, у вас может быть:

public int IncrementByRandomAmount(int input)
{
    // We can't do anything if we're given int.MaxValue
    Contract.Requires(input < int.MaxValue);
    Contract.Ensures(Contract.Result<int>() > input);

    // Do stuff here to compute output
    return output;
}

В переписанном коде будет проверка в точке возврата, чтобы гарантировать, что возвращаемое значение действительно больше, чем вход.