Dafny中循环内断言不成立但循环前断言成立的原因探究

问题的核心在于Dafny中old操作符的作用域规则：

• 方法内非循环区域的old(expr)，引用的是方法入口时expr的初始值。
• 循环体内部的old(expr)，引用的是每次进入循环体时expr的状态，而非方法入口的初始状态。

具体拆解 #

循环前的断言 #

循环前的语句执行后，p_k的值为1，此时的old(a[..])指向方法刚启动时的数组初始状态。由于我们刚修改了a[0]（对应p_k-1=0），old(a[..])[0]+1必然等于当前的a[0]，因此断言成立。

循环内的断言 #

进入循环后，每次执行赋值语句a[(k)-1], k, p_k := ...后，p_k的值是当前循环迭代前的k值。但此时循环内的old(a[..])是进入本次循环体时的数组状态——这个状态已经是上一次迭代修改后的结果，而非方法入口的初始状态。此时old(a[..])[(p_k)-1]加1，自然不等于当前的a[(p_k)-1]（因为当前又对该位置做了一次+1操作），所以断言失败。

修正方案 #

如果要在循环内持续引用方法入口的数组初始状态，需要在方法开头用幽灵变量预先保存，而非依赖old操作符：

method m(a: array<int>, m: int)
modifies a;
requires 1 <= m <= a.Length;
{
    ghost var initial_a := a[..]; // 固定保存方法入口的数组初始状态
    var k: int := 1;
    ghost var p_k: int;
    a[(k)-1], k, p_k := a[(k)-1]+1, k+1, k;
    assert initial_a[(p_k)-1]+1 == a[(p_k)-1]; 
    while k <= m
    decreases m-k;
    invariant 2 <= k <= m+1;
    invariant 1 <= p_k < k;
    invariant initial_a[(p_k)-1]+1 == a[(p_k)-1]; 
    {
        a[(k)-1], k, p_k := a[(k)-1]+1, k+1, k;
        assert initial_a[(p_k)-1]+1 == a[(p_k)-1]; 
    }
}

通过initial_a固定指向方法启动时的数组状态，无论循环内外的断言都能通过验证。

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