Кодовые контракты не могут инвертировать условные обозначения?

У меня есть эта структура (упрощенная для краткости):

public struct Period
{
    public Period(DateTime? start, DateTime? end) : this()
    {
        if (end.HasValue && start.HasValue && end.Value < start.Value)
        {
            throw new ArgumentOutOfRangeException("end", "...");
        }
        Contract.EndContractBlock();

        this.start = start;
        this.end = end;
    }

    private readonly DateTime? start;
    private readonly DateTime? end;

    public static Period operator +(Period p, TimeSpan t)
    {
        Contract.Assume(!p.start.HasValue || !p.end.HasValue || p.start.Value <= p.end.Value);
        return new Period(
            p.start.HasValue ? p.start.Value + t : (DateTime?) null,
            p.end.HasValue ? p.end.Value + t : (DateTime?) null);
    }
}

Но статическая проверка дает мне это предупреждение:

CodeContracts: требует недоказанных: end.HasValue && & start.HasValue && end.Value >= start.Value

Это требование, которое оно выводит из проверки пользовательских параметров, просто неверно. Я хочу разрешить нулевые значения для start или end, и требуется только start <= end, если оба они предусмотрены. Однако, если я сменил конструктор на это:

public Period(DateTime? start, DateTime? end) : this()
{
    Contract.Requires(!start.HasValue || !end.HasValue || start.Value <= end.Value);
    this.start = start;
    this.end = end;
}

Я получаю это предупреждение, которое выглядит более правильным, но трудно понять, почему требования не могут быть доказаны:

CodeContracts: требует недоказанных:! start.HasValue ||! end.HasValue || start.Value <= end.Value

Я думал, что это может вызвать проблемы с ?:, но это предупреждение все еще существует, когда я меняю оператор на:

public static Period operator +(Period p, TimeSpan t)
{
    var start = p.start.HasValue ? p.start.Value + t : (DateTime?) null;
    var end = p.end.HasValue ? p.end.Value + t : (DateTime?) null;

    Contract.Assume(!start.HasValue || !end.HasValue || start.Value <= end.Value);
    return new Period(start, end);
}

И, конечно, если я изменю значение .Requires на .Assume, предупреждение полностью исчезнет, ​​но это не приемлемое решение.

Таким образом, кажется, что статическая проверка в Code Contracts не может правильно инвертировать условие. Вместо того, чтобы просто инвертировать условие, обернув его !(…) или применив закон Де Моргана (как показано выше), он, похоже, инвертирует только последний компонент условия, Не удается ли статическому контролеру корректно интерпретировать сложные условные выражения при использовании выборочной проверки параметров?

Интересно, что я пробовал это, думая, что статический контролер просто разделит ! с фронта, но нет:

if (!(!start.HasValue || !end.HasValue || start.Value <= end.Value))
{
    throw new ArgumentOutOfRangeException("end", "...");
}
Contract.EndContractBlock();

CodeContracts: требуется недоказанный:! (! (! start.HasValue ||! end.HasValue || start.Value <= end.Value))

В этом случае он просто завершил все условие с помощью !(…), даже если это не было.

Кроме того, если я изменяю значение nullable DateTime на простое значение, отличное от нуля, DateTime и переписываю такие контракты, он работает как ожидается без каких-либо предупреждений:

public struct Period
{
    public Period(DateTime start, DateTime end) : this()
    {
        Contract.Requires(start <= end);
        this.start = start;
        this.end = end;
    }

    private readonly DateTime start;
    private readonly DateTime end;

    public static Period operator +(Period p, TimeSpan t)
    {
        Contract.Assume(p.start + t <= p.end + t);   // or use temp variables
        return new Period(p.start + t <= p.end + t);
    }
}

Но просто использование Contract.Assume(p.start <= p.end) не будет работать.

CodeContracts: требует недоказанных: start <= end

Ответы

Ответ 1

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

Возьмем пример вашего одного конструктора:

public Period(DateTime? start, DateTime? end) : this()
{
    Contract.Requires(!start.HasValue || !end.HasValue || start.Value <= end.Value);
    this.start = start;
    this.end = end;
}

Что делать, если start.HasValue равно false (значение !start.HasValue равно true), но end имеет значение. Что оценивает start.value <= end.Value в этой ситуации, так как один имеет значение null, а другой имеет значение?

Кажется, что ваше условие Contract.Requires должно быть указано следующим образом:

Contract.Requires(!(start.HasValue && end.HasValue) || start.Value <= end.Value);

Если какой-либо из start или end не имеет значения, тогда условие возвратит true (и короткое замыкание на условие ИЛИ, никогда не оценивая, есть ли или нет start.value <= end.Value). Однако, если оба start и end имеют назначенное значение, первая часть условного возвращает false, в этом случае тогда start.Value должно быть меньше или равно end.Value, чтобы условное для оценки до true в целом. Это то, что вам нужно.

Вот вопрос для вас: верно ли, что для любого экземпляра Period требуется, чтобы start.value <= end.Value или один или другой (или оба) из них были null? Если это так, вы можете указать это как Инвариантный. Это означает, что при любом входе или выходе метода !(start.HasValue && end.HasValue) || start.Value <= end.Value должен иметь значение true. Это может значительно упростить ваши контракты, когда это сработает.

UPDATE

Обзор моей статьи в блоге Я разместил в комментариях (TDD и кодовые контракты), вы можете смело аннотировать вашу реализацию operator +(Period p, TimeSpan t) с помощью кода Контракты PureAttribute. Этот атрибут сообщает статическому анализатору Code Contracts, что метод не изменяет никакого внутреннего состояния объекта, на который вызван метод, и поэтому является свободным от побочных эффектов:

[Pure]
public static Period operator +(Period p, TimeSpan t)
{
    Contract.Requires(!(p.start.HasValue && p.end.HasValue) || p.start.Value <= p.end.Value)

    return new Period(
        p.start.HasValue ? p.start.Value + t : (DateTime?) null,
        p.end.HasValue ? p.end.Value + t : (DateTime?) null);
}

UPDATE

Хорошо, я подумал об этом еще немного, и я думаю, что теперь понимаю, что с контрактами Code Contracts есть с вашими контрактами. Я думаю, вам также нужно добавить к вашему конструктору контракт Contract.Ensures (т.е. Контракт условий сообщения):

public Period(DateTime? start, DateTime? end) : this()
{
    Contract.Requires(!(start.HasValue && end.HasValue) || start.Value <= end.Value);
    Contract.Ensures(!(this.start.HasValue && this.end.HasValue) || this.start.Value <= this.end.Value);
    this.start = start;
    this.end = end;
}

Это сообщает Code Contracts, что когда ваш конструктор выходит, поля start и end объекта, если они оба имеют значение, должны удовлетворять условию start.value <= end.Value. Если это условие не выполняется, (потенциально) исключение будет вызываться Кодовыми контрактами. Это также должно помочь статическому анализатору.

UPDATE (опять же, и в основном для полноты)

Я еще немного следил за "недоказанным" предупреждением. Это может произойти как для Requires, так и для Ensures. Вот еще один пример того, кто имеет аналогичную проблему: http://www.go4answers.com/Example/ensures-unproven-contractresult-79084.aspx.

Добавление инварианта контракта можно сделать следующим образом (для рассматриваемого кода OP):

[ContractInvariantMethod]
protected void PeriodInvariants()
{
    Contract.Invariant(!(start.HasValue && end.HasValue) || start.Value <= end.Value);
}

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

Еще одна запись в блоге, которая должна оказаться интересной

Я нашел еще одну запись в блоге от кого-то еще, которая может оказаться интересной: http://www.rareese.com/blog/net-code-contracts

В этом случае я не согласен с авторским "решением", чтобы избавиться от предупреждения requires unproven. Здесь авторский код:

public static void TestCodeContract(int value)
{
    if(value > 100 && value < 110)
        TestLimits(value); 
}

public static void TestLimits(int i)
{
    Contract.Requires(i > 100);
    Contract.Requires(i < 110);

    //Do Something
}

Здесь реальное решение проблемы должно быть следующим:

public static void TestCodeContract(int value)
{
    Contract.Requires(value > 100 && value < 110);
    // You could alternatively write two Contract.Requires statements as the blog
    // author originally did.
}

Это также должно избавиться от предупреждения, так как статический анализатор теперь знает, что value должен находиться в диапазоне от 101 до 109, что также соответствует критериям контракта метода TestLimits.

Поэтому мое предложение состоит в том, чтобы проверить, где вызывается конструктор Period, и/или метод Period.operator +(...), чтобы гарантировать, что вызывающий метод также имеет необходимые операторы Contract.Requires (или, альтернативно, Contract.Assume, который указывает статическому анализатору просто предположить, что предоставленное условие истинно).

При использовании кодовых контрактов вам необходимо задействовать весь ваш код. Обычно вы не можете "выбрать и выбрать", для какой части указать контракты, поскольку у статического анализатора, скорее всего, не будет достаточно информации для завершения анализа (и, следовательно, гарантируется, что контракты будут гарантированы), и вы получите много предупреждений.