为何Dafny判定错误的数组反转算法为正确？

错误原因 #

这段Dafny代码能通过验证但实际运行出错，核心问题有三点：

1. 循环范围错误：原代码循环条件是i < aLength，会遍历数组所有索引。但数组反转只需要交换前半部分和后半部分的对应元素，遍历到数组长度的一半即可，遍历全程会导致已经完成交换的元素被二次覆盖。
2. 赋值逻辑缺失：原代码仅执行a[aLength - 1 - i] := a[i]，没有保存a[aLength - 1 - i]的原始值，当循环到后半段时，赋值的是已经被修改过的a[i]，而非原数组的对应值。
3. 循环不变式不完整：原不变式只描述了前i个位置等于原数组的反转值，但未约束数组后半部分的状态，导致Dafny误判代码满足后置条件，忽略了后半部分被错误覆盖的问题。

以反例数组{1,3,5,7}为例：

• 当i=0时，a[3]被设为a[0]（值1），数组变为{1,3,5,1}
• 当i=1时，a[2]被设为a[1]（值3），数组变为{1,3,3,1}
• 当i=2时，a[1]被设为a[2]（此时a[2]已经是3），数组保持不变
• 当i=3时，a[0]被设为a[3]（值1），数组仍为{1,3,3,1}

修正方案 #

通用int类型版本 #

method reverse(a: array<int>)
    modifies a;
    ensures forall i :: 0 <= i < a.Length ==> a[i] == old(a[a.Length - 1 - i]);
{
    var i := 0;

    while i < a.Length / 2
        invariant 0 <= i <= a.Length / 2
        invariant forall k :: 0 <= k < i ==> a[k] == old(a[a.Length - 1 - k])
        invariant forall k :: i <= k < a.Length - i ==> a[k] == old(a[k])
        invariant forall k :: 0 <= k < i ==> a[a.Length - 1 - k] == old(a[k])
    {
        var v0 := a[i];
        var v1 := a[a.Length - 1 - i];

        a[i]                := v1;
        a[a.Length - 1 - i] := v0;

        i := i + 1;
    }
}

适配C#原生sint32类型的高性能版本 #

predicate is_sint32(x : int) { -0x8000_0000 <= x < 0x8000_0000 }

newtype {:nativeType "int"} sint32 = x : int | -0x8000_0000 <= x < 0x8000_0000

method reverse(a: array<sint32>)
    requires is_sint32(a.Length)
    modifies a;
    ensures forall i :: 0 <= i < a.Length ==> a[i] == old(a[a.Length - 1 - i]);
{
    var aLength     := a.Length as sint32;
    var aLengthDiv2 := aLength / 2;
    var i           := 0 as sint32;

    while i < aLengthDiv2
        invariant 0 <= i <= aLengthDiv2
        invariant forall k :: 0 <= k < i ==> a[k] == old(a[aLength - 1 - k])
        invariant forall k :: i <= k < aLength - i ==> a[k] == old(a[k])
        invariant forall k :: 0 <= k < i ==> a[aLength - 1 - k] == old(a[k])
    {
        var v0 := a[i];
        var v1 := a[aLength - 1 - i];

        a[i]               := v1;
        a[aLength - 1 - i] := v0;

        i := i + 1;
    }
}

修正要点 #

• 循环范围改为i < aLength / 2，只遍历前半部分索引
• 增加临时变量保存待交换的两个元素的原始值，避免覆盖后丢失数据
• 补充完整的循环不变式，约束未处理区域的元素保持原值，同时确认已交换区域的元素符合反转要求，让Dafny能正确验证代码正确性

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