dafny - 为什么 Dafny 认为这个不正确的算法是正确的？

Question

以下数组反转代码已被 Dafny“证明是正确的”，但显然不正确。我做错了什么？

一个反例是数组:

var a = new int[4] {1,3,5,7};

预期结果 {7,5,3,1} 和实际结果 {1,3,3,1}:

// A method reversing an array

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

newtype {:nativeType "int"} sint32 = x | -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 i       := 0 as sint32;
    var aLength := a.Length as sint32;

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

        i := i + 1;
    }
}

我找到了一个解决方案，其灵感来自 James Wilcox 的出色回答。在此处添加以供将来引用:

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# 代码时使用 C# native 类型以获得最佳性能的解决方案:

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;
    }
}

Answer 1

问题是 old(a)[...] 并不代表你的想法。查看reference manual section on old expressions .

简短的版本是 old 仅 影响“堆取消引用”，其中包括字段访问(如 old(x.f))和数组访问(如 old(a[i]) 中所示)。

由于您对 old 的使用不包含括号内的任何字段或数组访问，因此它们没有执行任何操作。您的后置条件相当于:

ensures forall i :: 0 <= i < a.Length ==> a[i] == a[a.Length - 1 - i]

(简单删除了old)，意思是这个方法运行后，a保证是回文。您的代码确实满足此规范，但它不是您打算编写的规范。