Опитвам се да разбера кодовите договори малко по-подробно. Имам следния измислен пример, където се опитвам да твърдя инварианта на шаблон 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);
Мога да получа напълно чиста компилация с кодови договори само ако използвам дългия начин за изразяване на това подробно по-горе. Въпросът ми е защо!
