Контракты на код: как я могу указать в постусловии, что значение поля / свойства не изменилось?

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