loop-invariant - 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;
  }
}

给定的错误如下：“这个循环不变量可能不会被循环维护。” 我想我可能需要另一个不变量，但我认为我的代码除此之外是正确的（我猜）。任何帮助表示赞赏。提前致谢。

Answer 1

每当评估循环分支条件时，必须保持循环不变量。但是在循环的最后一次迭代中，i实际上是n+1，所以循环不变量不是真的。

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

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