不确定为什么 Dafny 验证失败

Question

function method abs(m: int): nat
{ if m>0 then m else -m }

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
    invariant 0<=res
    invariant res <=5*abs(m)
    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;
  }
}

我试图增加循环中的不变性。在第一个循环中，我添加了条件 res<=5*abs(m) 但 Dafny 抱怨说 "This loop invariant might not be maintained by the loop." 我不明白这是怎么回事。

我可能做错了什么？

Answer 1

如果您通过在每次迭代后准确说明 res 等于什么来使循环不变性更强，Dafny 将能够验证它。

所以在第一个 while 循环中，使用 invariant res == 5*abs(m) - 5*m1 而不是 invariant res <= 5*abs(m)。当循环终止时，m1 等于零，因此 res 将是 5*abs(m).

同样，对于第二个while循环，定义invariant res == 5*m - 3*n + 3*n1。现在，当此循环终止时，n1 等于零，因此 res 将为 5*m - 3*n，Dafny 将能够证明该方法的 post 条件成立。

P.S。我通常使用 > 0 而不是 != 0 作为循环条件。

进行这些更改后，您将拥有：

function method abs(m: int): nat
{
    if m > 0 then m else -m
}

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;
        invariant 0 <= res;
        invariant res == 5*abs(m) - 5*m1;
        decreases m1;
    {
        res := res + 5;
        m1 := m1 - 1;
    }
    if (m < 0)
    {
        res := -res;
    }

    while (n1 > 0)
        invariant n1 >= 0;
        invariant res == 5*m - 3*n + 3*n1;
        decreases n1;
    {
        res := res - 3;
        n1 := n1 - 1;
    }
}

在 Dafny 中验证。

不确定为什么 Dafny 验证失败

Unsure why this Dafny verification fails

dafny