如果您通过在每次迭代后准确地说明res等于什么来增强循环不变量，那么Dafny将能够验证它。
因此，在第一个while循环中，使用invariant res == 5*abs(m) - 5*m1而不是invariant res <= 5*abs(m)。当循环结束时，m1等于0，因此res将为5*abs(m)。
类似地，对于第二个while循环，定义invariant res == 5*m - 3*n + 3*n1。现在，当此循环终止时，n1等于0，因此res将为5*m - 3*n，Dafny将能够证明该方法的后置条件成立。
附注:我通常使用> 0而不是!= 0作为循环条件。
进行这些更改后，您将拥有：
代码语言：javascript复制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;
}
}这在达夫尼得到了验证。