【问题标题】:Ensures that object is unchanged?确保对象不变?
【发布时间】:2012-11-09 12:46:48
【问题描述】:

有没有办法使用代码契约来确保/检查方法不会更改对象的任何成员,类似于 C++ const 方法或将所有成员设置为 readonly?

即比以下更简单的方法:

Contract.Ensures(this.member1 == Contract.OldValue(this.member1));
Contract.Ensures(this.member2 == Contract.OldValue(this.member2));
Contract.Ensures(this.member3 == Contract.OldValue(this.member3));
Contract.Ensures(this.member4 == Contract.OldValue(this.member4));
Contract.Ensures(this.member5 == Contract.OldValue(this.member5));

或同样使用Contract.EnsuresOnThrow。

【问题讨论】:

  • C#: Can parameters be constant? 的可能重复项
  • @Sjoerd 我不认为这是重复的,因为这里的 Op 专门询问是否可以使用代码合同来完成。
  • @Sjoerd:我不是在问语言/编译器是否可以执行此检查,我知道它不能。我在问代码合同静态/运行时检查是否可以做到这一点。

标签: c# .net code-contracts


【解决方案1】:

所以本质上你想检查方法是Pure。 official documentation 表示它尚不支持(参见第 5.4 节):

5.4 Purity

All methods called within a contract must be pure: that is, they must not update
any pre-existing state. (A pure method is allowed to modify objects that have been
created after entry into the pure method.) Code Contract tools currently assume
the following things are pure:

* Methods marked [Pure] (If a type is marked [Pure], then that applies to all of
  its methods.) The pure attribute is dened in the contract library. (Section 4.3)

* Property getters.

* Operators (static methods whose names start with op , have one or two parameters
  and a non-void return type).

* Any method whose fully qualified name begins with
  System.Diagnostics.Contracts.Contract, System.String, System.IO.Path, or
  System.Type.

* Any invoked delegate, provided that the delegate type itself is attributed with
  [Pure]. The existing delegate types System.Predicate<T> and System.Comparison<T>
  are considered pure.

In the future, there will be a purity checker that will enforce these assumptions.

【讨论】:

  • 也许您可以包含相应的内容以完成您的答案?
  • @ronag - 抱歉,说得好。我已将文档添加到答案中。
  • 大概是 "dened" == "defined" :)
  • 我猜 - 它是直接从文档中复制而来的。
【解决方案2】:

如果你的类实现了

ICloneable

和

IEquatable<YourClassType>

作为值相等(不是引用相等),你可以这样写:

Contract.Ensures( 
    this.Equals ( Contract.OldValue ( (YourClassType)this.Clone() )
);

【讨论】:

    猜你喜欢
    • 1970-01-01
    • 1970-01-01
    • 1970-01-01
    • 1970-01-01
    • 1970-01-01
    • 1970-01-01
    • 1970-01-01
    • 1970-01-01
    • 1970-01-01
    相关资源
    最近更新 更多