c# - 在 C# 代码合约中使用纯函数时的静态验证限制？

Question

我正在尝试使用代码契约静态验证以下基于数组的堆栈的部分实现。方法Pop()使用纯函数IsNotEmpty()以确保后续数组访问将处于/高于下限。静态验证器失败并建议我添加前提条件 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;
    }
}

Answer 1

这应该可以解决问题:

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

请参阅代码合约论坛上的此帖子以获取更多信息:Calling a method in Contract.Requires

编辑:

这个问题的另一个解决方案，如上面链接的线程中提到的，是 -infer 命令行选项:

Now, inferring the post condition of this method is possible, and in fact we do have the option to do so: try to add -infer ensures on the extra options line in the contract property pane for the static checker.

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

-infer (requires + propertyensures + methodensures) (default=propertyensures)