1

当我验证以下程序片段时，其中有一个错误， 下面转载的达夫尼方法

我从 BVD 得到以下结果，我不明白。

BVD 结果

令我困惑的是，第二个不变量似乎在生成反例时被忽略了。如果两个不变量是 I0 和 I1 并且保护是 G，那么验证条件肯定是 I0 && I1 && !G ==> qy > x 并且反例应该满足这个否定。我误解了什么？

为了方便任何想要它的人，下面复制了代码。

function TwoToThe( i : int ) : int
decreases i 
requires i >= 0
{
    if i==0 then 1 else 2*TwoToThe( i-1 )
}

method interestingBVD(x : int, y : int)
    requires y > 0 
    requires x >= 0
{
    var q := 1 ;
    var qy := y ; // Tracks q*y
    ghost var i := 0 ;
    // Double q until q*y exceeds x
    while( qy < x )  // Off by one error.
        invariant qy == q*y
        invariant q == TwoToThe(i)
        decreases 2*x-qy ;
    {
        q, qy, i := 2*q, 2*qy, i + 1 ;
    }
    // In the BVD we get actual numbers!!
    assert q*y == qy > x && q == TwoToThe(i) ; 
}
4

1 回答 1

1

验证调试器指出qy可能相等x，特别是它们可能都相等2988。确实，!G在您的评论中是x <= qy，不是qy > x。

当我们在这个例子中时，还有另一个值得注意的问题：

从第二个不变量，验证者确实知道q == TwoToThe(i). 这是预期的，可以使用 进行测试assert，就像您所做的那样。换句话说，验证者知道q等于申请的TwoToThe结果i。验证调试器显示q和i具有值2988和5330。这可能看起来很奇怪，因为我们知道它TwoToThe(5330)远大于2988。那么，这里发生了什么？

要计算 的值TwoToThe(5330)，必须展开TwoToThe5330 次的定义。验证者不会尝试多次展开定义，因此据它所知，2988仍然会出现 的合理值。TwoToThe(5330)在调试失败的验证时，这可能是有用的信息。

总之，验证调试器提供对验证者世界的洞察，即洞察验证者“在想”什么。在这里，我们可以看到它“认为”TwoToThe(5330)返回2988。然后，我们反过来了解到，要么的定义TwoToThe不是它的名字所暗示的那样，要么验证者没有完全扩展TwoToThe确定值所需的数千个递归调用。

鲁斯坦

于 2018-11-21T18:36:44.743 回答