自动实现的属性的代码合同

Question

有没有办法将合同放在.NET中自动实现的属性上？(如果答案是'是'怎么办？)？

(我假设使用DevLabs的.NET代码合同)

Answer 1

是的,这是可能的 - 所需要的只是将您的合同条件添加到[ContractInvariantMethod]您的类中的方法,然后将等效的Requires前提条件添加到自动setter,并将post条件Ensures添加到get.参考文献的 2.3.1节

如示例所示,自动属性的不变量变为:

1. 设定者的前提条件
2. 吸气剂的后置条件
3. 底层支持字段的不变量

并举例说明:

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 );
...

Answer 2

谢谢波吉斯。

我的错误是我实际上使用了ReleaseRequires选项，它确实只处理方法的 通用Requires<T>版本， .

放在自动实现的属性上的不变性实际上变成了 Requires前提条件，但它不是通用的 - 这就是为什么它无法使用此选项。

该怎么办：

• 变体 1. 考虑使用代码片段和可爱的Requires<T>属性而不是自动实现的属性 - 这使我们能够使用所需类型的异常。

• VARIANT 2.将选项更改 ReleaseRequires为Preconditions代码契约的选项，并随意在自动属性上编写不变量 - 重写器工具会自动将它们更改为Requires. 然而，它们将是非通用的——这意味着，如果合同被破坏，aContractException将被抛出，并且没有办法改变这种行为。

感谢大家的帮助！