Dafny循环不变式构建困惑：数组归位方法的验证问题

目标明确 #

你的方法核心是把数组中能归位的元素放到a[i] = i的位置，超出数组索引范围的元素无需处理，同时保证元素多重集不变——这个核心需求没问题。

外循环不变式补全 #

你现有的外循环不变式只覆盖了索引范围和多重集，但缺少关键的逻辑约束。需要添加：

• 所有k < n的位置，要么a[k] = k，要么a[k]不在[0, a.Length)区间内

完整外循环不变式：

invariant 0 <= n <= a.Length
invariant multiset(a[..]) == multiset(old(a[..]))
invariant forall k :: 0 <= k < n ==> (a[k] = k || a[k] < 0 || a[k] >= a.Length)

这个不变式明确：外循环走到n时，前n个位置已经彻底处理完毕，不会再被后续操作修改。

内循环不变式设计 #

内循环的作用是通过交换，把当前a[n]（如果是有效索引且未归位）推到正确位置，同时接收被换出来的元素继续处理。需要的不变式包括：

1. 当前处理的索引n始终在有效范围内：0 <= n < a.Length
2. 前n个位置的处理状态保持不变（继承外循环的约束）
3. 数组多重集始终和初始状态一致
4. 只要当前a[n]是有效索引，它就还没归位（对应循环条件）

完整内循环不变式：

invariant 0 <= n < a.Length
invariant forall k :: 0 <= k < n ==> (a[k] = k || a[k] < 0 || a[k] >= a.Length)
invariant multiset(a[..]) == multiset(old(a[..]))
invariant (0 <= a[n] < a.Length) ==> (a[a[n]] != a[n])

后置条件确认 #

你当前的multiset(a[..]) == multiset(old(a[..]))完全正确，不需要修改。如果要让方法的功能描述更清晰，可以额外添加一个后置条件，明确最终状态：

ensures forall i :: 0 <= i < a.Length ==> (a[i] = i || (a[i] < 0 || a[i] >= a.Length))

这个条件直接说明：最终数组里，每个有效索引位置要么元素归位，要么元素本身就不属于数组索引范围，没法归位。

完整可验证代码 #

method foo(a: array<int>)
    modifies a
    ensures multiset(a[..]) == multiset(old(a[..]))
    ensures forall i :: 0 <= i < a.Length ==> (a[i] = i || (a[i] < 0 || a[i] >= a.Length))
{
    var n := 0;

    while n != a.Length
        invariant 0 <= n <= a.Length
        invariant multiset(a[..]) == multiset(old(a[..]))
        invariant forall k :: 0 <= k < n ==> (a[k] = k || a[k] < 0 || a[k] >= a.Length)
    {
        while 0 <= a[n] < a.Length && a[a[n]] != a[n]
            invariant 0 <= n < a.Length
            invariant forall k :: 0 <= k < n ==> (a[k] = k || a[k] < 0 || a[k] >= a.Length)
            invariant multiset(a[..]) == multiset(old(a[..]))
            invariant (0 <= a[n] < a.Length) ==> (a[a[n]] != a[n])
        {
            a[n], a[a[n]] := a[a[n]], a[n];
        }
        n := n + 1;
    }
}

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