Dafny 程序的 BVD 的奇怪（？）结果

Question

当我验证以下程序片段时，其中有一个错误，

我从 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) ; 
}

Answer 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)的值，需要将TwoToThe的定义展开5330次。验证器不会多次尝试展开定义，因此据它所知，2988 仍然显示出合理的值 TwoToThe(5330)。在调试失败的验证时，这可能是有用的信息。

总而言之，Verification Debugger 提供了对 The World According to the Verifier 的洞察，即洞察验证者是什么 "thinking"。在这里，我们可以看到"thinks"TwoToThe(5330)returns2988。然后，我们反过来了解到 TwoToThe 的定义不是它的名字所暗示的那样，或者验证者没有完全扩展确定值所需的 TwoToThe 的数千次递归调用。

鲁斯坦

Dafny 程序的 BVD 的奇怪（？）结果

Strange (?) result from the BVD for a Dafny program

dafny