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?

Gilson

Answer 1

Contract.OldValue should be enough:

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

Cowboy