Кодовые контракты на автоматически реализованные свойства

Ответ 1

Спасибо Porges.

Моя ошибка заключалась в том, что я действительно использовал параметр ReleaseRequires, который действительно имеет дело только с generic версией метода Requires<T>.

Инвариант, который помещается в автоматически реализованное свойство, действительно превращается в предварительное условие Requires, но он не является общим - почему он не работает с использованием этой опции.

Что делать:

• VARIANT 1. Рассмотрите возможность использования фрагментов кода и прекрасных Requires<T> вместо автоматически реализованных свойств, что позволяет нам использовать исключения желаемого типа.

• VARIANT 2. Измените параметр ReleaseRequires на Preconditions в параметрах кода контракта и не стесняйтесь записывать инварианты в автоматические свойства - инструмент перезаписи автоматически изменит их в Requires. Тем не менее, они будут неэквивалентными - это означает, что в случае нарушения контракта будет отклонен ContractException, и нет никакого способа изменить это поведение.

Спасибо всем за помощь!

Ответ 2

Да, это возможно - все, что необходимо, - это добавить условие контракта к методу [ContractInvariantMethod] в вашем классе, которое затем добавляет эквивалентное условие Requires к автоматическому set ter, и условие сообщения Ensures добавляется к get. Из раздела 2.3.1 Ссылка

Как показывает пример, инварианты на авто-свойствах превращаются в:

• Предварительное условие для установщика
• Постусловие для геттера
• Инвариант для базового поля поддержки

И на примере:

public int MyProperty { get; private set ;}

[ContractInvariantMethod]
private void ObjectInvariant ()
{
  Contract.Invariant ( this.MyProperty >= 0 );
}

"эквивалентен следующему коду:"

private int backingFieldForMyProperty;
public int MyProperty 
{
  get 
  {
    Contract.Ensures(Contract.Result<int>() >= 0);
    return this.backingFieldForMyProperty;
  }

  private set 
  {
    Contract.Requires(value >= 0);
    this.backingFieldForMyProperty = value;
  }
}

[ContractInvariantMethod]
private void ObjectInvariant () 
{
  Contract.Invariant ( this.backingFieldForMyProperty >= 0 );
...

Ответ 3

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