代码合同:如何在后置条件中声明字段/属性的值未发生变化？

Question

我最好只用一个代码示例来展示我想要实现的目标？

class SomeClass
{
    public int SomeProperty;

    public void SomeOperation()
    {
        Contract.Ensures( "SomeProperty's value has not changed." );
                     //   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
                     //    How can I write this post-condition?
    }
};

(传递给的字符串Contract.Ensures()当然只是真正的后置条件表达式的占位符.)

我怎样才能做到这一点？将Contract.OldValue<>()在这里任何使用的？

Answer 1

Contract.OldValue 应该够了:

Contract.Ensures(this.SomeProperty == Contract.OldValue(this.SomePropety));