CodeContracts: повторное использование предположений/утверждений?

Я разместил это на Форум CodeContracts в MSDN, но, по-видимому, никто не знает и не удосуживается изучить эту проблему.

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

[ContractVerification(false)]
public static class Assert
{
    [Conditional("DEBUG")]
    public static void GreaterThan<T>(T value, T lowerBound) where T : IComparable<T>
    {
        Contract.Ensures(value.CompareTo(lowerBound) > 0);
    }

    [Conditional("DEBUG")]
    public static void GreaterThanOrEqual<T>(T value, T lowerBound) where T : IComparable<T>
    {
        Contract.Ensures(value.CompareTo(lowerBound) >= 0);
    }

    [Conditional("DEBUG")]
    public static void LessThan<T>(T value, T upperBound) where T : IComparable<T>
    {
        Contract.Ensures(value.CompareTo(upperBound) < 0);
    }

    [Conditional("DEBUG")]
    public static void LessThanOrEqual<T>(T value, T upperBound) where T : IComparable<T>
    {
        Contract.Ensures(value.CompareTo(upperBound) <= 0);
    }

    [Conditional("DEBUG")]
    public static void NotNull(object value)
    {
        Contract.Ensures(value != null);
    }

    [Conditional("DEBUG")]
    public static void NotNullOrEmpty(string value)
    {
        Contract.Ensures(!string.IsNullOrEmpty(value));
    }

    [Conditional("DEBUG")]
    public static void True(bool value)
    {
        Contract.Ensures(value);
    }

    [Conditional("DEBUG")]
    public static void False(bool value)
    {
        Contract.Ensures(!value);
    }

    [Conditional("DEBUG")]
    public static void InRange<T>(T value, T lowerBound, T upperBound, ExclusionMode exclusionMode = ExclusionMode.None) where T : IComparable<T>
    {
        Contract.Ensures(((exclusionMode | ExclusionMode.LowerBound) == ExclusionMode.LowerBound ? value.CompareTo(lowerBound) > 0 : value.CompareTo(lowerBound) >= 0) && ((exclusionMode | ExclusionMode.UpperBound) == ExclusionMode.UpperBound ? value.CompareTo(upperBound) < 0 : value.CompareTo(upperBound) <= 0));
    }
}

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

[ContractVerification(false)]
public static class Assert
{
    [Conditional("DEBUG")]
    public static void GreaterThan(int value, int lowerBound)
    {
        Contract.Ensures(value > lowerBound);
    }

    [Conditional("DEBUG")]
    public static void GreaterThanOrEqual(int value, int lowerBound)
    {
        Contract.Ensures(value >= lowerBound);
    }

    [Conditional("DEBUG")]
    public static void LessThan(int value, int upperBound)
    {
        Contract.Ensures(value < upperBound);
    }

    [Conditional("DEBUG")]
    public static void LessThanOrEqual(int value, int upperBound)
    {
        Contract.Ensures(value <= upperBound);
    }

    [Conditional("DEBUG")]
    public static void NotNull(object value)
    {
        Contract.Ensures(value != null);
    }

    [Conditional("DEBUG")]
    public static void NotNullOrEmpty(string value)
    {
        Contract.Ensures(!string.IsNullOrEmpty(value));
    }

    [Conditional("DEBUG")]
    public static void True(bool value)
    {
        Contract.Ensures(value);
    }

    [Conditional("DEBUG")]
    public static void False(bool value)
    {
        Contract.Ensures(!value);
    }

    [Conditional("DEBUG")]
    public static void InRange(int value, int lowerBound, int upperBound, ExclusionMode exclusionMode = ExclusionMode.None)
    {
        Contract.Ensures(((exclusionMode | ExclusionMode.LowerBound) == ExclusionMode.LowerBound ? value > lowerBound : value >= lowerBound) && ((exclusionMode | ExclusionMode.UpperBound) == ExclusionMode.UpperBound ? value < upperBound : value <= upperBound));
    }
}

Мне просто нужно объяснение, а не решение, это связано с тем, что CodeContracts работает не напрямую с исходным кодом, а с IL?


c# assert code-contracts
person Eyal Alon    schedule 25.07.2012    source источник

Ответы (1)


arrow_upward
2
arrow_downward

То, что вы хотите, вполне возможно, но мало кто об этом знает. Сначала перейдите на свой компьютер к C:\Program Files (x86)\Microsoft\Contracts\Languages\CSharp и включите ContractExtensions.cs в свой проект. Он содержит некоторые атрибуты, которые вам нужны.

Затем примените к своим методам атрибут ContractAbbreviator. . Вы можете удалить атрибуты [Conditional("DEBUG")] и [ContractVerification(false)], поскольку вы можете установить поведение контракта для отладки и выпуска на странице свойств Code Contracts вашего проекта. Обратите внимание, что вы должны вызывать свои контрактные методы в начале метода, где в противном случае вы написали бы контракты. Вы не можете поместить какой-либо другой код в методы.

public static class Assert
{
    [ContractAbbreviator]
    public static void GreaterThan<T>(T value, T lowerBound)
        where T : IComparable<T>
    {
        Contract.Ensures(value.CompareTo(lowerBound) > 0);
    }

    // ...
}

Хотя это ответ на ваш вопрос, он может не решить вашу проблему. Причина в том, что средство статической проверки не может видеть это, когда a.CompareTo(b) > 0, a > b держится. Таким образом, этот пример не будет работать с вашей универсальной версией, но будет работать с вашей неуниверсальной версией:

static int PlusOne(int value)
{
    #region Contract
    Contract.Requires(value > 0);
    Assert.GreaterThan(value, 0);
    #endregion
    return value + 1;
}

Редактировать:

Видимо, я совершенно неправильно понял ваши намерения с классом Assert. Вы действительно можете сделать то, что было рекомендовано на этот форум.

Однако нельзя ожидать, что статический чекер поймет, что, например, из x.CompareTo(y) > 0 следует тот x > y. Причина? Вы можете поместить буквально что угодно в эти методы. Например:

public int CompareTo(MyType t)
{
    // Implementation not consistent with '>'
    return this.field1 == t.field1 ? -1 : 1;
}

public static operator bool >(MyType left, MyType right)
{
    // Implementation not consistent with CompareTo()
    return left.CompareTo(right) <= 0;
}

Возможно, у вас даже нет CompareTo. Так что статичный чекер не может увидеть сходство между ними.

person Daniel A.A. Pelsmaeker    schedule 27.07.2012
comment
Я уже писал, что работает с неуниверсальной версией, я это знаю. Я работаю с CodeContracts с тех пор, как он был выпущен, и я знаю, что ваш пример не будет работать, статическая проверка будет жаловаться на эти утверждения, потому что ContractAbbreviator работает только с требованиями и никогда не был разработан для обеспечения или чего-либо еще. В вашем примере вы утверждаете после контракта, что бессмысленно, точка утверждения проверяет вывод другой функции сразу после ее вызова. - person Eyal Alon; 31.07.2012
comment
Ваш пример работает, потому что статическая проверка уже проверила ввод, в середине нет функции, возвращающей произвольное значение, которое необходимо подтвердить. Я не прошу решения, я прошу этого человека сказать мне, почему универсальная версия не работает? почему его не видно? какое ограничение? - person Eyal Alon; 31.07.2012
comment
Вы видите это неправильно. ContractAbbreviator может работать как с требует, так и с обеспечивает. Только с атрибутом ContractAbbreviator контракты в GreaterThan вставляются прямо там, где выполняется вызов метода. Это не утверждение (но вы назвали его Assert) и не после контракта. Это часть контракта. PlusOne в моем примере есть один requires и один обеспечивает (через GreaterThan). В итоге GreaterThan никогда не будет вызываться, копируются только контракты. И я рассказал вам, почему чекер не может работать и с CompareTo, и с операторами сравнения. - person Daniel A.A. Pelsmaeker; 31.07.2012
comment
Что ж, я дважды проверил это, и вы правы. ContractAbbreviator может работать для обеспечения, но я не просто пошел и назвал его утверждением, они на самом деле используются для утверждений, как если бы вы использовали Contract.Assume и тот, кто сказал мне сделать это Франческо на форуме CodeContracts, когда я конкретно спросил, как я могу создавать многоразовые предположения. social.msdn.microsoft. com/Forums/en-US/codecontracts/thread/ - person Eyal Alon; 31.07.2012
comment
Когда я использую ContractAbbreviator, он не работает должным образом, потому что статическая проверка жалуется, когда не должна, она должна работать точно так же, как если бы я использовал Contract.Assume, и приведенная выше реализация делает это очень хорошо. При всем уважении ничего нового вы мне не сказали, я хочу знать, почему он не может вычислить выражение и умничать? Я знаю, что у него есть ограничение и что он не может его оценить, но почему? Я ценю ваше время. - person Eyal Alon; 31.07.2012