当无法证明属性时，如何告诉静态检查器属性永远不会改变？

Question

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

关键是属性永远不变确实无法证明。我个人可以“发誓”它永远不会改变（并且我也对其进行了单元测试），但它无法被正式证明（或者至少我认为如此）。

考虑以下简化示例：

    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. Add Contract.Ensures( c.SomeProp == Contract.OldValue( c.SomeProp ) ) to 方法，以及接受 SomeClass 类型参数的所有其他方法。
   人们很容易看出这是多么荒谬。

2. 在第二次调用 Method(c) 之前添加对 c.SomeProp == 5 的冗余检查。
   虽然这不像第一个选项那么荒谬，但它也是不可接受的，因为除了使代码变得混乱之外，它还会带来性能损失（这样的检查不会被优化掉）。

理想的解决方案是以某种方式说服检查器 SomeProp 在构造后永远不会改变，但我找不到任何方法来做到这一点。

或者也许我在这里遗漏了一些明显的东西？

Answer 1

像这样重写它：

public class SomeClass
{
    private readonly int _someProp;

    public int SomeProp { get { return _someProp; } }

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