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

本文关键字：属性 getter 调用 Contracts Code 静态 静态分析 不平等 分析器 为什么 | 更新日期: 2023-09-27 18:08:49

我试图建立一个不可变的有序单链列表类使用代码契约来强制排序。我遇到了一些问题，可以归结为这个例子:

[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。

如上面第二条注释所述，通过向ChildProperty getter添加后置条件Contract.Ensures(Contract.Result<Hierarchy>().Data == _child.Data);来解决这个问题。注意，这就是我们所需要做的——在本例中，代码契约识别出，当x == y在x和y上调用Data getter时，将产生相同的结果。

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

是bug吗?我是否错过了一些合约注释或其他允许断言Child.Data == _child.Data被证明的东西?换句话说，有没有别的办法解决这个问题?

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

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

可能是因为Data属性不保证不改变_data的内容(虽然它是readonly，但其内容仍然可能是可变的)?

例如，假设您有:

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

那么随后两次调用Data会得到不同的结果。

是否将此添加到Data的get工作?

Contract.Ensures(_data == Contract.OldValue<object>(_data));
相关文章：