c# - コード コントラクト: フィールド/プロパティの値が変更されていないことを事後条件で述べるにはどうすればよいですか?

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