求助：如何用Dafny证明基于交换的排序算法正确性？

问题分析 #

你遇到的assert j+1 < a.Length断言失败，核心原因是该断言本身不成立——当j等于a.Length-1时，j+1等于a.Length，并不小于数组长度。此外，你使用的内层循环不变式Inv(a[..],j,A)不符合算法实际行为，导致后续断言无法通过验证。

关键修正点 #

1. 移除无效断言：直接删除assert j+1 < a.Length;这一行，它没有任何逻辑依据。
2. 重新定义循环不变式：
   • 外层循环不变式：跟踪前i个元素已排序，且数组的多重集与原始输入一致。
   • 内层循环不变式：针对固定的i，确保前i个元素保持有序，数组多重集不变，且当前a[i]大于等于已遍历过的所有元素。

修正后的验证代码 #

predicate Sorted(q: seq<int>)
{
    forall i,j :: 0 <= i <= j < |q| ==> q[i] <= q[j]
}

predicate InvOuter(a: array<int>, i: nat, A: multiset<int>)
{
    i <= a.Length &&
    multiset(a) == A &&
    Sorted(a[..i])
}

predicate InvInner(a: array<int>, i: nat, j: nat, A: multiset<int>)
{
    j <= a.Length &&
    multiset(a) == A &&
    Sorted(a[..i]) &&
    forall l < j :: a[i] >= a[l]
}

method {:verify true} SomeSort(a: array<int>, ghost A: multiset<int>)
    requires multiset(a[..]) == A
    ensures Sorted(a[..])
    ensures multiset(a[..]) == A
    modifies a
{
    var i := 0;
    while i != a.Length
        invariant InvOuter(a, i, A)
        decreases a.Length - i
    {
        var j := 0;
        while j != a.Length
            invariant InvInner(a, i, j, A)
            decreases a.Length - j
        {
            if a[i] < a[j]
            {
                a[i], a[j] := a[j], a[i]; // swap
            }
            j := j + 1;
        }
        i := i + 1;
    }
}

验证逻辑说明 #

• 外层循环不变式InvOuter：每次外层循环迭代后，前i个元素已按非降序排列，且数组元素的多重集始终与原始输入一致。
• 内层循环不变式InvInner：在遍历j的过程中，前i个元素的有序性不会被破坏（仅当j >=i时才可能交换，且交换不影响前i个元素），同时保证a[i]是已遍历元素中的最大值。
• 内层循环终止后：a[i]会成为整个数组的最大值，此时前i+1个元素自然保持有序，满足外层循环不变式的更新要求。
• 外层循环终止后：i等于数组长度，意味着整个数组已按非降序排列，且多重集不变，满足方法的后置条件。

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