数组副本想要修改源
问题描述:
在下面的代码中,将数组的一个片段复制到另一个数组中,指示源数组保留的循环不变量不会被验证。数组副本想要修改源
这与this question和this other one有关,但我还没有发现任何在这种情况下工作。
method copy
(a: array<int>, a0: nat,
b: array<int>, b0: nat,
len: nat)
requires a != null && b != null
requires a0 + len <= a.Length
requires b0 + len <= b.Length
modifies b
{
var i := 0;
while i < len
decreases len - i
invariant i <= len
invariant a[..] == old(a[..])
{
b[b0 + i] := a[a0 + i];
i := i + 1;
}
}
答
您需要添加一个前提a != b
。否则,如果a
和b
是别名,则该方法可能确实修改了a
。