在C＃代码合同中使用纯函数时的静态验证限制？

我想静态验证以下代码合同的基于数组的堆栈的部分实现。方法Pop()使用纯函数IsNotEmpty()来确保后续的数组访问将位于/高于下限。静态验证器失败并建议我添加前提条件Contract.Requires(0 <= this.top)。在C＃代码合同中使用纯函数时的静态验证限制？

任何人都可以解释为什么验证者无法证明该数组访问是有效的下限给定合同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; 
    } 
}

来源

2010-09-12 Todd Schiller

个人而言，我是一个对代码合同有点失望... – ChaosPandion 2010-09-12 16:37:53

ChaosPandion，有什么令人失望的？ – 2010-09-12 17:17:15

即使当类没有标记为'sealed'时，继承类*不能*覆盖'IsNotEmpty'，因为它没有标记为'virtual'，所以在那里没有问题。 – 2010-09-12 17:53:04

这应该解决的问题：

[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命令行选项：

现在，推断该方法的后置条件是可能的，而事实上，我们也必须做这样的选择：尝试添加-infer确保了在约定财产多余行选项面板为静态检查器。

我检查过了，这确实可以解决问题。如果您查看code contracts manual，您会看到默认选项仅用于推断属性后置条件。通过此开关，你可以告诉它试图推断的方法事后条件太：

-infer（需要+ propertyensures + methodensures）（默认值= propertyensures）

来源

2010-09-12 17:42:01 Rich

感谢Rich，你知道为什么属性的行为不同吗？ – 2010-09-12 18:17:07

@Todd席勒：是的，请看我编辑的答案。 – Rich 2010-09-13 01:07:52

该条件更简单地写为：'Contract.Result （）==（0 <= this.top）'。 – porges 2010-09-14 22:22:08

在C＃代码合同中使用纯函数时的静态验证限制？

回答

相关问题