Пользовательские методы в Contract.Ensures - PullRequest
Новая
       36

Пользовательские методы в Contract.Ensures

3 голосов
/ 05 декабря 2011

Я пытаюсь понять кодовые контракты немного подробнее. У меня есть следующий надуманный пример, где я пытаюсь утвердить инвариант шаблона try / get: если он возвращает true, тогда объект out не равен NULL, в противном случае, если он возвращает 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);

Я могу получить полностью чистую компиляцию с контрактами кода, только если я использую многословный способ выразить это подробно выше. У меня вопрос почему!

Ответы [ 2 ]

1 голос
/ 05 декабря 2011

Конечно, вы также можете попробовать Contract.Ensures(Contract.Result<bool>() == (Contract.ValueAtReturn(out fruit) != null)); У меня есть смутное воспоминание, что анализатор предпочитает == другим операторам.

Я добился некоторого успеха, отследив эти вещи с помощью Contract.Assert, который помогает вам выяснить, где находится дыра в анализе. Я также нашел случаи, когда Contract.Assert позволяет анализу быть успешным. Другими словами, вы можете исправить это с помощью пары утверждений: 

public static bool TryParseFruit(string maybeFruit, out Fruit fruit) 
{ 
    Contract.Requires(maybeFruit != null); 

    Contract.Ensures(Implies(Contract.Result<bool>(), Contract.ValueAtReturn(out fruit) != null);

    // Elided for brevity 
    if (ICanParseIt()) 
    { 
        fruit = SomeNonNullValue; 
        Contract.Assert(Implies(Contract.Result<bool>(), Contract.ValueAtReturn(out fruit) != null);
        return true; 
    } 
    else 
    { 
        fruit = null; 
        Contract.Assert(Implies(Contract.Result<bool>(), Contract.ValueAtReturn(out fruit) != null);
        return false; 
    } 
}

Грязный, я знаю. С другой стороны, если какое-либо утверждение не выполняется, вы можете посмотреть, например, на другие аспекты логики. Например, вы можете засорить свой код с помощью Contract.Assert(SomeNonNullValue != null);, чтобы увидеть, где анализатор теряет уверенность в ненулевом значении SomeNonNullValue.

EDIT

Если Assert недоказан, но вы знаете, что это должно быть доказуемо, то вы можете использовать это, чтобы помочь локализовать проблему. Я подозреваю, что проблема (или, по крайней мере, ее часть) заключается в отсутствии у вас Ensures в методе Implies. Попробуйте добавить Contract.Ensures(Contract.Result<bool>() == (Contract.OldValue(a) == Contract.OldValue(b))); Кроме того, поскольку у меня снова есть смутные воспоминания о различной обработке для разных логических операторов, попробуйте повторить возвращение этого метода. Например: return a == b;

1 голос
/ 05 декабря 2011

Прежде всего, ваше условие может быть сжато без использования специального метода: 

Contract.Ensures(Contract.Result<bool>() ^ (Contract.ValueAtReturn(out fruit) == null));

(Здесь ^ - это оператор XOR )

Теперь оваш вопрос.Я думаю, что очень трудно сказать, в чем причина, если вы точно не знаете, как работает статический верификатор.Там могут быть сотни ограничений.С моей точки зрения, верификатор Code Contracts каким-то образом останавливается на границах методов.Я имею в виду, что верификатор не изучает метод Implies и не знает, что он делает.Поэтому он не может получить то, что он возвращает в каждом случае.И когда вы добавляете метод в метод, он получает возможность полностью проверять код.Но, опять же, я думаю, что никто за пределами команды разработчиков точно не знает.

ОБНОВЛЕНИЕ

Как было выяснено в комментариях, оператор XOR, кажется,не поддерживается текущей версией CodeContracts.Удачи в следующий раз ...

...