arrays - 数组副本要修改源

Question

在以下将数组切片复制到另一个切片的代码中，表明源数组已保留的循环不变量未验证。

这与这个问题和另一个问题有关，但我还没有找到任何适用于这种情况的东西。

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

Answer 1

您需要添加一个前提条件，即a != b. 否则，如果a和b有别名，那么该方法可能确实会修改a.