2

我正在尝试使用代码合同静态验证基于数组的堆栈的以下部分实现。该方法Pop()使用纯函数IsNotEmpty()来确保后续数组访问将处于/高于下限。静态验证器失败并建议我添加 precondition Contract.Requires(0 <= this.top)。

谁能解释为什么验证者不能证明数组访问对于给定合同的下限是有效的IsNotEmpty()？

起初我认为这种Contract.Requires(IsNotEmpty())方法可能不正确，因为子类可以覆盖IsNotEmpty(). 但是，如果我将类标记为sealed.

更新：如果我更改IsNotEmpty()为只读属性，则验证按预期成功。这就提出了一个问题：只读属性和纯函数如何/为什么被区别对待？ 

class StackAr<T>
{
    private T[] data;
    private int capacity;

    /// <summary>
    /// the index of the top array element
    /// </summary>
    private int top;

    [ContractInvariantMethod]
    private void ObjectInvariant()
    {
        Contract.Invariant(data != null);
        Contract.Invariant(top < capacity);
        Contract.Invariant(top >= -1);
        Contract.Invariant(capacity == data.Length);
    }

    public StackAr(int capacity)
    {
        Contract.Requires(capacity > 0);
        this.capacity = capacity;
        this.data = new T[capacity];
        top = -1;
    }

    [Pure]
    public bool IsNotEmpty()
    {
        return 0 <= this.top;
    }

    public T Pop()
    {
        Contract.Requires(IsNotEmpty());

        //CodeContracts: Suggested precondition: 
        //Contract.Requires(0 <= this.top);

        T element = data[top];
        top--;
        return element;
    }
}
4

1 回答 1

4

这应该可以解决问题：

[Pure]
public bool IsNotEmpty() {
    Contract.Ensures(Contract.Result<bool>() && 0 <= this.top || !Contract.Result<bool>() && 0 > this.top);
    return 0 <= this.top;
}

有关更多信息，请参阅代码合同论坛上的此线程：调用 Contract.Requires 中的方法

编辑：

如上面链接的线程中所述，此问题的另一个解决方案是-infer命令行选项：

现在，推断此方法的后置条件是可能的，实际上我们确实可以选择这样做：尝试在静态检查器的合同属性窗格中的额外选项行中添加 -infer ensure。

我已经检查过了，这确实解决了问题。如果您查看代码合同手册，您会看到默认选项是仅推断属性后置条件。通过使用此开关，您可以告诉它也尝试推断方法的后置条件：

-infer (需要 + propertyensures + methodensures) (默认=propertyensures)

于 2010-09-12T17:42:01.603 回答