Dafny Einfügemethode, eine Nachbedingung möglicherweise nicht auf diesem Rückweg halten

Question

Ich habe ein Array "Zeile", die eine Zeichenfolge enthält in ihm der Länge "l" und ein Array "nl", die eine Zeichenfolge enthält Länge enthält "p". Hinweis: "l" und "p" müssen nicht unbedingt die Länge jedes entsprechenden Arrays sein. Der Parameter "at" ist die Position, an der die Einfügung innerhalb der "Zeile" erfolgt. Fortsetzen: Ein Array der Länge "p" wird in "Zeile" eingefügt und verschiebt alle Zeichen der "Zeile" zwischen Position (at, i, an + p), "p" Positionen nach rechts, um die Einfügung zu machen .

Meine Logik für die Sicherstellung ist zu prüfen, ob die in "line" eingefügten Elemente die gleiche Reihenfolge haben und dieselben sind wie die in "nl" enthaltenen Zeichen.

Hier ist the code:

method insert(line:array<char>, l:int, nl:array<char>, p:int, at:int) 
    requires line != null && nl != null; 
    requires 0 <= l+p <= line.Length && 0 <= p <= nl.Length ; 
    requires 0 <= at <= l; 
    modifies line; 
    ensures forall i :: (0<=i<p) ==> line[at+i] == nl[i]; // error 
{ 
    var i:int := 0; 
    var positionAt:int := at; 
    while(i<l && positionAt < l) 
    invariant 0<=i<l+1; 
    invariant at<=positionAt<=l; 
    { 
    line[positionAt+p] := line[positionAt]; 
    line[positionAt] := ' '; 
    positionAt := positionAt + 1; 
    i := i + 1; 
    } 

    positionAt := at; 
    i := 0; 
    while(i<p && positionAt < l) 
    invariant 0<=i<=p; 
    invariant at<=positionAt<=l; 
    { 
    line[positionAt] := nl[i]; 
    positionAt := positionAt + 1; 
    i := i + 1; 
    } 
} 

Hier die errors sind, die ich empfangen werde.

Danke.

Answer 1

Ich vermute, dass Ihr Algorithmus nicht korrekt ist, weil es nicht der Tatsache Rechnung zu tragen scheint, dass die Zeichen Verschiebung beginnend an Position at von p Orte könnten sie über das Ende der Zeichenfolge in line schreiben.

Meine Erfahrung ist, dass, um mit der Überprüfung erfolgreich zu sein

1. Gute Standards der Code-Entwicklung sind von entscheidender Bedeutung. Gute Variablennamen, Codeformatierungen und andere Code-Konventionen sind noch wichtiger als üblich.
2. Schreiben von Code, der logisch einfach ist, ist sehr hilfreich. Versuchen Sie, überflüssige zusätzliche Variablen zu vermeiden. Versuche, arithmetische und logische Ausdrücke zu vereinfachen, wo immer es praktikabel ist.
3. Starten mit einem korrekten Algorithmus erleichtert die Überprüfung. Das ist natürlich leichter gesagt als getan!
4. Es ist oft hilfreich, die stärksten Loop-Invarianten auszugeben, die Ihnen einfallen.
5. Oft ist es hilfreich, von der Nachbedingung rückwärts zu arbeiten. In Ihrem Fall nehmen Sie die Nachbedingung und die Negation der letzten Schleifenbedingung - und verwenden Sie diese, um herauszufinden, was die Invariante der letzten Schleife sein muss, um die Nachbedingung zu implizieren. Dann rückwärts von dieser zur vorherigen Schleife usw.
6. Wenn man Arrays manipuliert, ist die Verwendung einer Geistervariablen, die den ursprünglichen Wert des Arrays als Sequenz enthält, sehr oft eine effektive Strategie. Ghost-Variablen erscheinen nicht in der Compiler-Ausgabe und beeinflussen nicht die Leistung Ihres Programms.
7. Es ist oft hilfreich, Assertionen für den genauen Zustand des Arrays aufzuschreiben, auch wenn die Nachbedingung nur eine schwächere Eigenschaft erfordert.

Hier ist ein bestätigtes Umsetzung Ihrer gewünschten Vorgang:

// l is length of the string in line 
// p is length of the string in nl 
// at is the position to insert nl into line 
method insert(line:array<char>, l:int, nl:array<char>, p:int, at:int) 
    requires line != null && nl != null 
    requires 0 <= l+p <= line.Length // line has enough space 
    requires 0 <= p <= nl.Length // string in nl is shorter than nl 
    requires 0 <= at <= l // insert position within line 
    modifies line 
    ensures forall i :: (0<=i<p) ==> line[at+i] == nl[i] // ok now 
{ 
    ghost var initialLine := line[..]; 

    // first we need to move the characters to the right 
    var i:int := l; 
    while(i>at) 
    invariant line[0..i] == initialLine[0..i] 
    invariant line[i+p..l+p] == initialLine[i..l] 
    invariant at<=i<=l 
    { 
    i := i - 1; 
    line[i+p] := line[i]; 
    } 

    assert line[0..at] == initialLine[0..at]; 
    assert line[at+p..l+p] == initialLine[at..l]; 

    i := 0; 
    while(i<p) 
    invariant 0<=i<=p 
    invariant line[0..at] == initialLine[0..at] 
    invariant line[at..at+i] == nl[0..i] 
    invariant line[at+p..l+p] == initialLine[at..l] 
    { 
    line[at + i] := nl[i]; 
    i := i + 1; 
    } 

    assert line[0..at] == initialLine[0..at]; 
    assert line[at..at+p] == nl[0..p]; 
    assert line[at+p..l+p] == initialLine[at..l]; 
} 

http://rise4fun.com/Dafny/ZoCv