Überprüfen eine Dafny Methode, die einen Bereich eines Arrays verschiebt

Question

I Dafny bin mit einer Löschmethode zu machen, wo Sie erhalten:

• char-Array line

• die Länge des Arrays l

• eine Position at

• die Anzahl der Zeichen zu del ete p

Zuerst die Zeichen der Linie von an zu at + p, löschen und dann müssen Sie alle Zeichen auf der rechten Seite von at + p-at bewegen.

Zum Beispiel, wenn Sie [e][s][p][e][r][m][a] haben, und at = 3 und p = 3, dann sollte das Endergebnis sein [e][s][p][a]

Ich versuche, eine Nachbedingung zu beweisen, die Sinn macht wie:

ensures forall j :: (at<=j<l) ==> line[j] == old(line[j+p]);

Um sicherzustellen, dass alle Zeichen von rechts von + p in den neuen Positionen sind.

Aber Dafny gibt zwei Fehler:

Index außerhalb des zulässigen Bereichs 7 53

Nachbedingung möglicherweise nicht auf diesem Rückpfad halten. 2 19

method delete(line:array<char>, l:int, at:int, p:int) 
    requires line!=null; 
    requires 0 <= l <= line.Length && p >= 0 && at >= 0; 
    requires 0 <= at+p <= l; 
    modifies line; 
    ensures forall j :: (at<=j<l) ==> line[j] == old(line[j+p]) ; 
{ 
    var tempAt:int := at; 
    var tempAt2:int := at; 
    var tempPos:int := at+p; 
    while(tempAt < at + p) 
    invariant at<=tempAt<=at + p; 
    { 
    line[tempAt] := ' '; 
    tempAt := tempAt + 1; 
    } 

    while(tempPos < line.Length && tempAt2 < at + p) 
    invariant at + p<=tempPos<=line.Length; 
    invariant at<=tempAt2<=at+p; 
    { 
    line[tempAt2] := line[tempPos]; 
    tempAt2 := tempAt2 + 1; 
    line[tempPos] := ' '; 
    tempPos := tempPos + 1; 
    } 
} 

Here is the program on rise4fun

Answer 1

Ich glaube nicht, ist es notwendig, quantifiers zu verwenden, um solche Nachbedingungen auszudrücken. Sie werden normalerweise besser ausgedrückt, indem das Array in Sequenzen geschnitten wird.

Wenn Sie versuchen, eine Schleife zu überprüfen, müssen Sie eine Schleifeninvariante bereitstellen, die stark genug ist, um die Nachbedingung zu implizieren, wenn sie mit der Negation der Schleifenbedingung kombiniert wird.

Eine gute Strategie für die Auswahl einer Schleifeninvariante ist die Verwendung der Methode postcondition, wobei jedoch der Schleifenindex die Arraylänge ersetzt.

Ihre Schleifeninvariante muss auch stark genug sein, damit die Induktion funktioniert. In diesem Fall müssen Sie nicht nur angeben, wie die Schleife die Linie ändert, sondern auch, welche Teile der Linie in jeder Iteration gleich bleiben.

Solution on rise4fun.

// line contains string of length l 
// delete p chars starting from position at 
method delete(line:array<char>, l:nat, at:nat, p:nat) 
    requires line!=null 
    requires l <= line.Length 
    requires at+p <= l 
    modifies line 
    ensures line[..at] == old(line[..at]) 
    ensures line[at..l-p] == old(line[at+p..l]) 
{ 
    var i:nat := 0; 
    while(i < l-(at+p)) 
    invariant i <= l-(at+p) 
    invariant at+p+i >= at+i 
    invariant line[..at] == old(line[..at]) 
    invariant line[at..at+i] == old(line[at+p..at+p+i]) 
    invariant line[at+i..l] == old(line[at+i..l]) // future is untouched 
    { 
    line[at+i] := line[at+p+i]; 
    i := i+1; 
    } 
} 

Überschreiben mit Leerzeichen

Wenn Sie den hinteren Teil der alten Zeichenfolge mit Leerzeichen überschrieben werden soll, dies tun:

method delete(line:array<char>, l:nat, at:nat, p:nat) 
    requires line!=null 
    requires l <= line.Length 
    requires at+p <= l 
    modifies line 
    ensures line[..at] == old(line[..at]) 
    ensures line[at..l-p] == old(line[at+p..l]) 
    ensures forall i :: l-p <= i < l ==> line[i] == ' ' 
{ 
    var i:nat := 0; 
    while(i < l-(at+p)) 
    invariant i <= l-(at+p) 
    invariant at+p+i >= at+i 
    invariant line[..at] == old(line[..at]) 
    invariant line[at..at+i] == old(line[at+p..at+p+i]) 
    invariant line[at+i..l] == old(line[at+i..l]) // future is untouched 
    { 
    line[at+i] := line[at+p+i]; 
    i := i+1; 
    } 

    var j:nat := l-p; 
    while(j < l) 
    invariant l-p <= j <= l 
    invariant line[..at] == old(line[..at]) 
    invariant line[at..l-p] == old(line[at+p..l]) 
    invariant forall i :: l-p <= i < j ==> line[i] == ' ' 
    { 
    line[j] := ' '; 
    j := j+1; 
    } 
} 

Extended solution on rise4fun.