Is it possible to specify code contracts to ensure that method doesn't change state of object

Question

Lets say I got a boolean IsValid property on my object.

I would like to create a method, and ensure that IsValid isn't changed after calling it, whether it was true or false before the call.

Is there a support for such thing?

Answer 1

For that purpose the [Pure] Attribute has been added to the System.Diagnostic.Contracts Namespace. See here for further explanation. However you cannot prevent a single property from being changed. The method is not allowed to change the object state at all (like the C++ const).

EDIT: Unfortunately the Pure attribute does not work with the current tools. I implemented a test with the following code, no error message either at static nor at runtime type checking:

public class Test
{
    private int x = 0;

    [Pure]
    public void Foo()
    {
        x++;
    }
}

Regarding to the documentation of Pure checks will be supported 'in the future'. Whenever that is ("The Code Contracts team is working heavy on that, thus to come up with a purity checker in a future release.").

I have been using the attribute in the believe it works properly. The documentation says that all methods called within a contract must be declared as pure. It doesn't say whether that's checked or not.

So the answer to your question is: There is no current support for this, but may be in the future.