Contratos de código: ¿Cómo declaro en una condición posterior que el valor de un campo/propiedad no ha cambiado?

Question

Voy a mostrar con un ejemplo de código lo que me gustaría lograr?

class SomeClass 
{ 
    public int SomeProperty; 

    public void SomeOperation() 
    { 
     Contract.Ensures("SomeProperty's value has not changed."); 
        // ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 
        // How can I write this post-condition? 
    } 
}; 

(La cadena que se pasa a Contract.Ensures() es, por supuesto, sólo un marcador de posición para el verdadero post-expresión de condición.)

¿Cómo puedo hacer esto? ¿Sería de utilidad el Contract.OldValue<>() aquí?

Answer 1

Contract.OldValue debería ser suficiente:

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