Code Contracts: How do I state in a post-condition that a field/property's value has not changed?

Question

I'll best just show with a code example what I would like to accomplish? ``` class SomeClass { public int SomeProperty; public void SomeOperation() { Contract.Ensures( "SomeProperty's value has not changed." ); // ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ // How can I write this post-condition? } }; ``` (The string passed to `Contract.Ensures()` is of course just a placeholder for the real post-condition expression.) How can I do this? Would `Contract.OldValue<>()` be of any use here?

Accepted Answer

`Contract.OldValue` should be enough:

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

Code Contracts: How do I state in a post-condition that a field/property's value has not changed?

Solution

Problem