我的愚蠢方法有什么问题。简单方法后置条件可能不成立

Question

我是 Dafny 的新手，我正在尝试在不使用 *.

谁能告诉我我的代码有什么问题？我认为是不变量和减少。

method CalcTerm(m: int, n: nat) returns (res: int)
  ensures res == 5*m-3*n;
{
  var m1: nat := abs(m);
  var n1: nat := n;
  res := 0;

  while (m1!=0)
    invariant m1>=0
    decreases m1
  {
    res := res+5;
    m1 := m1-1;
  }

  if (m<0) { res := -res; }

  while (n1!=0)
    invariant n1 >= 0
    decreases n1
  {
    res := res-3;
    n1 := n1-1;
  }
}

但它一直在说：

A postcondition might not hold on this return path. 29  2

Answer 1

您说得对，问题与循环不变量有关。我建议阅读Guide 中关于断言和循环不变量的两个部分。

Dafny仅使用它的不变量来“总结”循环的效果。所以在你的方法中的第二个循环之后，Dafny 只会知道n1 >= 0 并且循环已经终止，所以实际上是n1 == 0。这不足以证明你的后置条件：你需要一个更强的不变量。这是一个可以帮助您取得进步的方法

invariant res == 5 * m - 3 * (n - n1)

这个不变量计算res 的值，根据循环到目前为止执行了多少次迭代 (n - n1)。如果您将此不变量添加到第二个循环，您将收到一个新错误（进度！），表示它可能无法进入。这意味着 Dafny 能够证明您的后置条件，但无法在第一个循环完成后确定新的不变量为真。这又是因为第一个循环的不变量太弱了。

也许这为您提供了足够的信息来尝试自己为第一个循环提出另一个不变量。如果您遇到困难，请随时在此处提出更多问题。