3

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

[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);到ChildPropertygetter 来解决问题。请注意，这就是我们需要做的所有事情——在这种情况下，代码契约认识到，当 时，在 x 和 y 上x == y调用getter 将产生相同的结果。Data

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

它是一个错误吗？我是否错过了一些合同注释或其他Child.Data == _child.Data可以证明断言的内容？换句话说，有没有其他方法可以解决这个问题？

4

2 回答 2

3

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

于 2013-04-24T22:09:08.763 回答
0

可能是因为该Data属性不保证不会更改 的内容_data（尽管它是readonly，但它的内容仍然可能是可变的）？

例如，假设你有这个：

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

然后两个后续调用Data会得到不同的结果。

将其添加到Data'sget工作吗？

Contract.Ensures(_data == Contract.OldValue<object>(_data));
于 2013-04-12T21:52:07.510 回答