错误 BP5005:此循环不变性可能不由循环维护

Question

我是Dafny的新手。我不明白为什么我收到这条消息，x == Sum(i);我开始失去理智。以及为什么当if n==0 then 0 else n + Sum(n-1)变成if n==0 then 0 else n-1 + Sum(n-1)时它会编译

function Sum(n: nat): nat
{ 
if n==0 then 0 else n + Sum(n-1)
}
method ComputeSum(n: nat) returns (x: nat) 
ensures x == Sum(n);
{
x := 0;
var y := 0;
var i : nat := 0;
while i < n
invariant 0 <= i <= n && x == Sum(i);
{
x,y := y,x + y ;
i := i + 1;
}
}

Answer 1

您将x和y设置为 0，但从不增加它们，因此加法保持为 0。Dafny 正确地证明您的程序不满足规范。我建议您逐步完成程序，以n来修复错误。

Answer 2

关于你的第二个问题：如果你把if n==0 then 0 else n + Sum(n-1)改成if n==0 then 0 else n-1 + Sum(n-1)，Sum(n( 的值是每 n 个 0。这符合 ComputeSum，它为所有输入 n 返回 0。