代码契约：如何在后置条件中声明字段/属性的值未更改？

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