dafny 中的指数方法：可能无法保持不变量

Question

我开始学习 Dafny，我刚刚学习了不变量。我有这个代码：

function pot(m:int, n:nat): int
{
  if n==0 then 1
  else if n==1 then m
  else if m==0 then 0
  else pot(m,n-1) * m
} 
method Pot(m:int, n:nat) returns (x:int)
ensures x == pot(m,n)
{
  x:=1;
  var i:=0;
  if n==0 {x:=1;}
  while i<=n
  invariant i<=n;
  {
    x:=m*x;
    i:=i+1;
  }
}

给出的错误如下："This loop invariant might not be maintained by the loop."我想我可能需要另一个不变量，但我认为除此之外我的代码是正确的（我猜）。任何帮助表示赞赏。提前致谢。

Answer 1

每当评估循环分支条件时，循环不变量必须成立。但是在循环的最后一次迭代中，i 实际上是 n+1，因此循环不变式不成立。

将循环不变量更改为 i <= n + 1 或将循环分支条件更改为 i < n 将解决此特定问题。

之后，您还需要做一些工作来完成方法的正确性验证。如果您遇到困难，请随时提出更多问题。

dafny 中的指数方法：可能无法保持不变量

Exponential method in dafny: invariant might not be maintained

loop-invariant

dafny