如何告诉静态检查器一个属性在不可验证时永远不会更改?

我的类有一个在构造函数中初始化的属性,不应该更改。我的代码基周围的方法都接受该类作为参数,并依赖于满足特定条件的属性。

关键的一点是,这个属性永远不会改变,这真的是无法证明的。我可以亲自“发誓”它永远不会改变(我也有它的单元测试),但它不能被正式证明(或者至少我认为是这样)。

考虑以下简化示例:

    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
        }
    }

注意,第一个呼叫 Method() 从检查者那里得到一个OK,因为我已经在它之前检查了条件是否满足。
然而,第二个调用得到 未经证实 警告。我的猜测是,检查者假设 Method(c) 可能会改变 c.SomeProp 使它不再满足条件。

由此,我可以推断出两种可能的解决方法,我认为这两种方法都不可接受:

1. 添加 Contract.Ensures( c.SomeProp == Contract.OldValue( c.SomeProp ) ) 到 Method ,以及其他接受类型参数的方法 SomeClass .
   很容易看出这是多么荒谬。

2. 为添加冗余检查 c.SomeProp == 5 在第二次呼叫之前 方法(c) .
   虽然这不像第一个选项那么荒谬,但也不可接受,因为除了混乱的代码外,它还将受到性能惩罚(这样的检查不会被优化掉)。

理想的解决方案是以某种方式说服检查者 SomeProp 在建造之后是不应该改变的,但是我找不到任何方法来改变。

或者我错过了一些显而易见的东西?