(Dafny) 将一个数组的元素添加到另一个数组中 - 循环不变
(Dafny) Adding elements of an array into another - loop invariant
我有一个函数 sum
,它将两个数组 a
和 b
作为输入并修改 b
使得 b[i] = a[0] + a[1] + ... + a[i]
。我写了这个函数,想和 Dafny 一起验证一下。但是,Dafny 告诉我,我的循环不变量可能不会由循环维护。这是代码:
function sumTo(a:array<int>, n:int) : int
requires a != null;
requires 0 <= n < a.Length;
decreases n;
reads a;
{
if (n == 0) then a[0] else sumTo(a, n-1) + a[n]
}
method sum(a:array<int>, b:array<int>)
requires a != null && b != null
requires a.Length >= 1
requires a.Length == b.Length
modifies b
ensures forall x | 0 <= x < b.Length :: b[x] == sumTo(a,x)
{
b[0] := a[0];
var i := 1;
while i < b.Length
invariant b[0] == sumTo(a,0)
invariant 1 <= i <= b.Length
//ERROR : invariant might not be maintained by the loop.
invariant forall x | 1 <= x < i :: b[x] == sumTo(a,x)
decreases b.Length - i
{
b[i] := a[i] + b[i-1];
i := i + 1;
}
}
我该如何解决这个错误?
如果 a
和 b
引用同一个数组,您的程序将不正确。您需要先决条件 a != b
。 (如果您添加它,Dafny 将验证您的程序。)
鲁斯坦
我有一个函数 sum
,它将两个数组 a
和 b
作为输入并修改 b
使得 b[i] = a[0] + a[1] + ... + a[i]
。我写了这个函数,想和 Dafny 一起验证一下。但是,Dafny 告诉我,我的循环不变量可能不会由循环维护。这是代码:
function sumTo(a:array<int>, n:int) : int
requires a != null;
requires 0 <= n < a.Length;
decreases n;
reads a;
{
if (n == 0) then a[0] else sumTo(a, n-1) + a[n]
}
method sum(a:array<int>, b:array<int>)
requires a != null && b != null
requires a.Length >= 1
requires a.Length == b.Length
modifies b
ensures forall x | 0 <= x < b.Length :: b[x] == sumTo(a,x)
{
b[0] := a[0];
var i := 1;
while i < b.Length
invariant b[0] == sumTo(a,0)
invariant 1 <= i <= b.Length
//ERROR : invariant might not be maintained by the loop.
invariant forall x | 1 <= x < i :: b[x] == sumTo(a,x)
decreases b.Length - i
{
b[i] := a[i] + b[i-1];
i := i + 1;
}
}
我该如何解决这个错误?
如果 a
和 b
引用同一个数组,您的程序将不正确。您需要先决条件 a != b
。 (如果您添加它,Dafny 将验证您的程序。)
鲁斯坦