Eine Terminierungsmaßnahme für Suchen und Ersetzen in Dafny finden?

Question

Ich codiere a search and replace method, die Methoden zum Suchen, Löschen und Einfügen verwendet. Ich rufe diese drei Methoden an und bin mir nicht sicher, welche Vorbedingungen ich verwenden soll. Jede Hilfe wäre willkommen.

Voll Code:

 method searchAndReplace(line:array<char>, l:int, 
     pat:array<char>, p:int, 
     dst:array<char>, n:int)returns(nl:int) 
     requires line != null && pat!=null && dst!=null; 
     requires !checkIfEqual(pat, dst); 
     requires 0<=l<line.Length; 
     requires 0<=p<pat.Length; 
     requires 0<=n<dst.Length; 

     modifies line; 
     { 
      var at:int := 0; 
      var p:int := n; 

      while(at != -1) 
      invariant -1<=at<=l; 
      { 
      at := find(line, l, dst, n); 
      delete(line, l, at, p); 
      insert(line, l, pat, p, at); 
      } 

      var length:int := line.Length; 

      return length; 
     } 


     function checkIfEqual(pat:array<char>, dst:array<char>):bool 
     requires pat!=null && dst!=null; 
      reads pat; 
     reads dst; 
{ 
    if pat.Length != dst.Length then false 
    else forall i:nat :: i < pat.Length ==> pat[i] == dst[i] 
} 

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

     method find(line:array<char>, l:int, pat:array<char>, p:int) returns (pos:int) 
    requires line!=null && pat!=null 
    requires 0 <= l < line.Length 
    requires 0 <= p < pat.Length 
    ensures 0 <= pos < l || pos == -1 
{ 
    var iline:int := 0; 
    var ipat:int := 0; 
    pos := -1; 

    while(iline<l && ipat<pat.Length) 
    invariant 0<=iline<=l 
    invariant 0<=ipat<=pat.Length 
    invariant -1 <= pos < iline 
    { 
     if(line[iline]==pat[ipat] && (line[iline]!=' ' && pat[ipat]!=' ')){ 
      if(pos==-1){ 
       pos := iline; 
      } 
      ipat:= ipat + 1; 
     } else { 
     if(ipat>0){ 
      if(line[iline] == pat[ipat-1]){ 
      pos := pos + 1; 
      } 
     } 
     ipat:=0; 
     pos := -1; 
     } 
     if(ipat==p) { 
      return; 
     } 
     iline := iline + 1; 
    } 
    return; 
} 

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

Answer 1

Dies ist eine ziemlich schwierige Sache zu beweisen. Hier sind einige erste Ideen, die Ihnen helfen könnten.

Sie müssen ein Abschlussmaß für die Schleife finden. Ich würde vorschlagen, etwas wie ein Tupel der Anzahl der Vorkommen des Musters und der Länge der Saite zu verwenden.

Sie müssen sehr vorsichtig sein, dass die Ersetzung den Suchbegriff nicht enthält, andernfalls wird Ihre Schleife möglicherweise nicht beendet. Und selbst wenn es terminiert, ist es schwierig, eine Beendigungsmaßnahme zu finden, die sich bei jeder Iteration verringert.

Zum Beispiel sagen, ich will "fggf" durch "gg" in der Zeichenfolge "ffggff" ersetzen, das erste Mal um die Schleife habe ich 1 Auftreten von "fggf" und ersetzen "fggf" durch "gg "ergibt" fggf "- also habe ich noch ein Vorkommen! Das zweite Mal endet ich mit "gg".

Sie werden so etwas wie eine Funktion benötigen:

function occurences(line:array<char>, l:int, pat:array<char>, p:int) : int 
    reads line 
    requires line != null 
    requires pat != null 
    requires 0 <= l < line.Length 
    requires 0 <= p < pat.Length 

Und dann verwenden, die in der Schleife wie

ghost var matches := occurrences(line, l, dst, n); 

    while(at != -1) 
     decreases matches 
     invariant -1<=at<=l 
     invariant matches == occurrences(line, l, dst, n) 
    { 
     at := find(line, l, dst, n); 
     delete(line, l, at, p); 
     insert(line, l, pat, p, at); 
     matches := matches - 1; 
    } 

Aber, wie ich schon sagte, die Anzahl der Vorkommen von selbst ist nicht genug Beweisen Sie die Kündigung. Sie können eine beliebige Berechnung als Abschlussmaß verwenden. Solange es in jeder Schleifeniteration abnimmt und keine unendlichen absteigenden Ketten hat.