自动实现属性的代码合约

发布于 2024-10-29 06:02:13 字数 90 浏览 1 评论 0原文

有什么方法可以将契约放在 .NET 中自动实现的属性上吗？（如果答案是“是”怎么办）？

（我假设使用来自 DevLabs 的 .NET 代码合约）

原文

分享到QQ

分享到微博

如果你对这篇内容有疑问，欢迎到本站社区发帖提问参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。

发布评论

需要登录才能够评论，你可以免费注册一个本站的账号。

别闹i 2024-11-05 06:02:14

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

如示例所示，自动属性的不变量变为：
setter 的先决条件
吸气剂的后置条件
底层支持字段的不变量

举例来说：

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

Yes, this is possible - all that is needed is to add your contract condition to the [ContractInvariantMethod] method in your class, which then adds the equivalent Requires precondition to the automatic setter, and a post condition Ensures is added to the get. From section 2.3.1 of the Reference

As the example illustrates, invariants on auto-properties turn into:
A precondition for the setter
A postcondition for the getter
An invariant for the underlying backing field

And by example:

public int MyProperty { get; private set ;}

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

"Is equivalent to the following code:"

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

回复收藏 0 原文

眼眸印温柔 2024-11-05 06:02:14

我没有在想，但是您可以轻松地编写可以做到这一点的片段。如果您走此路线，这是一个免费的摘要编辑，这将使任务变得非常容易。

回复收藏 0 原文

多情癖 2024-11-05 06:02:14

谢谢波吉斯。

我的错误是我实际上使用了 ReleaseRequires 选项，该选项实际上只处理方法的通用版本，Requires。

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

该怎么做：

VARIANT 1. 考虑使用代码片段和可爱的 Requires 而不是自动实现的属性 - 这使我们能够使用所需类型的异常。
VARIANT 2. 将选项更改为代码契约选项中的ReleaseRequires为Preconditions，并随意在自动属性上编写不变量 -重写器工具会自动将它们更改为Requires。但是，它们将是非通用的 - 这意味着，如果合同被破坏，将抛出 ContractException 并且无法更改此行为。

感谢大家的帮助！