1
在下面的代碼中,將數組的一個片段複製到另一個數組中,指示源數組保留的循環不變量不會被驗證。數組副本想要修改源
這與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;
}
}