Dafny简单循环不变量编写：解决不变量不被维护的验证报错

你写的循环不变量本身数学上是成立的，无法通过Dafny验证的核心原因是不变量中包含整数除法运算，Dafny的SMT求解器无法自动证明除法对应的分子(a-N)*((a-N)+1)一定是偶数，因此无法确认不变量在迭代后仍然成立。

优化方案 #

可以将不变量变形为无除法的等价形式，适配Dafny的自动推导逻辑。变形推导过程如下：
将原不变量两侧同时乘以2，可化简得到等价式：
2*r == a*(a+1) - N*(N+1)
这个式子完全规避了除法运算，也更贴合题目给出的后置条件形式，Dafny可以直接验证其成立性。

完整可通过验证的代码 #

method doingMath(N: int, M: int) returns (s: int)
requires N <= M //given precondition
ensures 2*s == M*(M+1)-N*(N+1) //given postcondition
{
    var a: int := N;
    var r: int := 0;

    while a < M 
    invariant a <= M
    invariant 2*r == a*(a+1) - N*(N+1)
    {
        a := a+1;
        r := r+a;
    }
    return r;
}

验证逻辑说明 #

1. 初始化状态：a=N，r=0，代入不变量得2*0 == N*(N+1) - N*(N+1)，成立
2. 保持性：假设迭代前不变量成立，即2*r_old == a_old*(a_old+1) - N*(N+1)，迭代后a = a_old+1，r = r_old + a，代入可推导得不变量仍然成立
3. 终止性：循环终止时a == M，代入不变量直接得到2*r == M*(M+1) - N*(N+1)，正好匹配后置条件，验证通过。

内容的提问来源于stack exchange，提问作者nitowa