Я пытаюсь понять кодовые контракты немного подробнее. У меня есть следующий надуманный пример, где я пытаюсь утвердить инвариант шаблона try/get, что если он возвращает true, то объект out не является нулевым, в противном случае, если он возвращает false.
public static bool TryParseFruit(string maybeFruit, out Fruit fruit)
{
Contract.Requires(maybeFruit != null);
Contract.Ensures((Contract.Result<bool>() && Contract.ValueAtReturn(out fruit) != null) ||
(!Contract.Result<bool>() && Contract.ValueAtReturn(out fruit) == null));
// Elided for brevity
if (ICanParseIt())
{
fruit = SomeNonNullValue;
return true;
}
else
{
fruit = null;
return false;
}
}
Мне не нравится дублирование внутри Contract.Ensures, поэтому я хотел выделить для этого свой собственный метод.
[Pure]
public static bool Implies(bool a, bool b)
{
return (a && b) || (!a && !b);
}
Затем я изменил свой инвариант в TryParseFruit на
Contract.Ensures(Implies(Contract.Result<bool>(), Contract.ValueAtReturn(out fruit) != null);
Но это генерирует предупреждения о том, что «гарантия не доказана». Если я затем выполню встроенный рефакторинг моего метода Implies, то все снова будет в порядке.
Может ли кто-нибудь объяснить мне, почему это происходит? Я предполагаю, что это потому, что Contract.ValueAtReturn каким-то волшебным образом используется, что означает, что я не могу просто передать результат другой функции и ожидать, что она сработает.
(Обновление №1)
Я думаю, что все следующие Contract.Ensures выражают одно и то же (а именно, что если функция возвращает true, то fruit не равно нулю, иначе fruit равно null). Обратите внимание, что я использую только один из них одновременно :)
Contract.Ensures(Implies(Contract.Result<bool>(), Contract.ValueAtReturn(out fruit) != null));
Contract.Ensures(Contract.Result<bool>() == (Contract.ValueAtReturn(out fruit) != null));
Contract.Ensures(Contract.Result<bool>() ^ (Contract.ValueAtReturn(out fruit) == null));
Однако ни одно из приведенных выше действий Contract.Ensures не приводит к чистой компиляции приведенного ниже кода. Я хочу, чтобы Code.Contracts выражал, что fruit.Name не может быть нулевой ссылкой.
Fruit fruit;
while (!TryGetExample.TryParseFruit(ReadLine(), out fruit))
{
Console.WriteLine("Try again...");
}
Console.WriteLine(fruit.Name);
Я могу получить полностью чистую компиляцию с кодовыми контрактами только в том случае, если я использую многословный способ выражения этого, подробно описанного выше. Мой вопрос почему!
