loop-invariant - dafny 中的指数方法 : invariant might not be maintained

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将解决这个特定问题。

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