时间戳

首页 > 解决方案 > 错误 BP5005：循环可能不会维护此循环不变量

dafny - 错误 BP5005：循环可能不会维护此循环不变量

问题描述

我是达夫尼的新手。我不明白为什么我收到这条消息时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;

    }
 }

标签： dafny

解决方案

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

推荐阅读