c# - 为什么 Code Contracts 静态分析器不平等对待这些属性 getter 调用？

Question

我正在尝试使用代码契约来设置一个不可变的有序单向链表类来强制执行排序。我遇到了一些归结为这个例子的问题:

[Pure, ContractVerification(true)]
public class Hierarchy
{
    private readonly object _data;
    private readonly Hierarchy _childField;

    public Hierarchy() { }

    public Hierarchy(object data, Hierarchy childParameter) {
        Contract.Requires<ArgumentNullException>(childParameter != null);

        _data = data;
        _childField = childParameter;

        Contract.Assert(HasChild);

        Contract.Assert(_childField == childParameter);
        Contract.Assert(_childField.Data == childParameter.Data);

        Contract.Assert(ChildProperty == _childField);
        Contract.Assert(ChildProperty.Data == _childField.Data);  //Warning -- CodeContracts: assert unproven
    }

    public bool HasChild { get { return _childField != null; } }

    public object Data {
        get {
            Contract.Ensures(Contract.Result<object>() == _data);
            return _data;
        }
    }

    public Hierarchy ChildProperty {
        get {
            Contract.Requires<InvalidOperationException>(HasChild);
            Contract.Ensures(Contract.Result<Hierarchy>() == _childField);

            //un-commenting this line causes the assertion to succeed.
            //Contract.Ensures(Contract.Result<Hierarchy>().Data == _childField.Data);

            return _childField;
        }
    }

    [ContractInvariantMethod]
    private void Invariant() {
        Contract.Invariant(HasChild == (ChildProperty != null));
    }
}

在我看来，代码合约应该能够证明断言 ChildProperty.Data == _childField.Data .较早的断言 ChildProperty == _childField成功，并调用纯 Data同一对象上的属性 getter 两次应该返回相同的结果。

另请注意(成功的)早期断言 _childField == childParameter和 _childField.Data == childParameter.Data .

如上面第二条评论所述，通过添加后置条件 Contract.Ensures(Contract.Result<Hierarchy>().Data == _child.Data); 解决了问题。到 ChildProperty setter/getter 。请注意，这就是我们需要做的所有事情——在这种情况下，代码合约会识别何时 x == y , 调用 Data x 和 y 上的 getter 将产生相同的结果。

这种解决方法对于这个小例子来说很好，但对于一个大类来说，必须为每个类型的属性添加一个后置条件是很麻烦的(更不用说有点愚蠢了)。

这是一个错误吗？我错过了一些契约(Contract)注释或其他允许断言 Child.Data == _child.Data 的东西吗？被证明？换句话说，有没有其他方法可以解决这个问题？

Answer 1

你完全正确。这应该是可以证明的，但不是由于静态检查器的限制。