Array copy wants to modify source

Question

In the following code that copies a slice of an array into another one, the loop invariant that tells that the source array is preserved does not validate.

This is related to this question and this other one, but I have not found anything that works in this case yet.

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

You need to add a precondition that a != b. Otherwise, if a and b are aliased, then the method might indeed modify a.