13

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

（我假设使用 DevLabs 的 .NET 代码合同）

4

3 回答 3

16

是的，这是可能的 - 只需将您的合同条件添加到[ContractInvariantMethod]您的类中的方法中，然后将等效的Requires前提条件添加到自动setter 中，并将后置条件Ensures添加到get. 来自参考资料的第 2.3.1 节

如示例所示，自动属性上的不变量变为：

  1. 设置器的先决条件
  2. getter 的后置条件
  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 );
...
于 2013-09-19T16:31:46.127 回答
1

我不这么认为，但是您可以轻松编写一个片段来执行此操作。如果你走这条路，这里有一个免费的代码段编辑器，它会让任务变得非常容易。

于 2011-04-01T13:27:25.153 回答
1

谢谢波热。

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

放在自动实现的属性上的不变量实际上变成了 Requires先决条件，但它不是通用的 - 这就是为什么它不能使用此选项工作的原因。

该怎么办：

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

  • 变体 2.将选项更改 ReleaseRequires为Preconditions代码合同的选项，并随意在自动属性上编写不变量 - 重写器工具会自动将它们更改为Requires. 但是，它们将是非通用的 - 这意味着，如果合同破裂，ContractException将抛出 a 并且无法更改此行为。

感谢大家的帮助！

于 2011-04-18T16:02:38.347 回答