Array-Kopie möchte die Quelle ändern

Question

Im folgenden Code, der ein Segment eines Arrays in ein anderes kopiert, wird die Schleifeninvariante, die angibt, dass das Quell-Array beibehalten wird, nicht validiert.

Das ist verwandt mit this question und this other one, aber ich habe nichts gefunden, das in diesem Fall noch funktioniert.

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

Sie brauchen eine Voraussetzung, dass a != b hinzuzufügen. Andernfalls, wenn a und b Aliasing sind, dann könnte die Methode tatsächlich a modifizieren.