코드 계약 : 사후 조건에서 필드/속성 값이 변경되지 않았 음을 어떻게 나타낼 수 있습니까?

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