How to tell the static checker that a property never changes when it is unprovable?

Question

My class has a property that is initialized in the constructor and is never supposed to change. Methods all around my codebase accept that class as a parameter and rely on that property satisfying a certain condition.

The key point is that it is really unprovable that the property never changes. I can personally "swear" that it never changes (and I have unit tests for it, too), but it cannot be proved formally (or at least I think so).

Consider the following reduced example:

    public class ConstantPoperty
    {
        public class SomeClass
        {
            public int SomeProp { 
                get { return GetSomePropThroughUnprovableMechanism(); }
            }

            public SomeClass( int i )
            {
                SetSomePropThroughUnprovableMechanism( i );
            }
        }

        public void Method( SomeClass c )
        {
            Contract.Requires( c != null );
            Contract.Requires( c.SomeProp == 5 );
        }

        public void FalsePositive()
        {
            SomeClass c = new SomeClass( 5 );
            if ( c.SomeProp != 5 ) return;
            Method( c );
            Method( c ); // unproven requires: c.SomeProp == 5
        }
    }

Note that the first call to Method() get an OK from the checker, since I've checked right before it that the condition is satisfied.
The second call, however, gets an unproven warning. My guess is, the checker assumes that the first call to Method(c) might change c.SomeProp so that it will no longer satisfy the condition.

From this, I can deduce two possible workarounds, neither of which I consider acceptable:

1. Add Contract.Ensures( c.SomeProp == Contract.OldValue( c.SomeProp ) ) to Method, as well as to every other method that accepts arguments of type SomeClass.
   One can easily see how this is absolutely ridiculous.

2. Add a redundant check for c.SomeProp == 5 before the second call to Method(c).
   While this is less ridiculous than the first option, it is also unacceptable, because in addition to cluttering the code, it will also have a performance penalty (such a check will not be optimized away).

The ideal solution would be to somehow convince the checker that SomeProp is never supposed to change after construction, but I couldn't find any way to do this.

Or maybe I am missing something obvious here?

Answer 1

Rewrite it like this:

public class SomeClass
{
    private readonly int _someProp;

    public int SomeProp { get { return _someProp; } }

    public SomeClass(int i)
    {
        _someProp = i;
    }
}