以下数组反转代码已被 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;
}
}
最佳答案
问题是 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
保证是回文。您的代码确实满足此规范,但它不是您打算编写的规范。
关于dafny - 为什么 Dafny 认为这个不正确的算法是正确的?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/73509939/