来自 Dafny 程序的 BVD 的奇怪 (?) 结果答案

【问题标题】：Strange (?) result from the BVD for a Dafny program来自 Dafny 程序的 BVD 的奇怪 (?) 结果
【发布时间】：2017-02-12 20:32:28
【问题描述】：

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

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

【问题讨论】：

标签： dafny

【解决方案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) 的合理值，据它所知。在调试失败的验证时，这可能是有用的信息。

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

鲁斯坦

【讨论】：