Trouver une mesure de résiliation pour Rechercher et remplacer dans Dafny?

Question

Je suis en train de coder a search and replace method en utilisant les méthodes find, delete et insert. J'appelle ces trois méthodes à l'intérieur d'un certain temps et je ne suis pas sûr de savoir quelles conditions préalables devrais-je utiliser. Toute aide serait appréciée.

complet 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

Ceci est une chose assez difficile à prouver. Voici quelques idées initiales qui pourraient vous aider.

Vous devez trouver une mesure de terminaison pour la boucle. Je suggère d'utiliser quelque chose comme un tuple du nombre d'occurrences du motif, et la longueur de la chaîne.

Vous devez veiller à ce que le remplacement ne contienne pas le terme de recherche, sinon votre boucle risque de ne pas se terminer. Et même si cela se termine, il est difficile de trouver une mesure de résiliation qui diminuera à chaque itération. Par exemple, disons que je veux remplacer "fggf" par "gg" dans la chaîne "ffggff", la première fois que j'aurai une occurrence de "fggf", et en remplaçant "fggf" par "gg" "résultats dans" fggf "- donc j'ai encore une occurrence! La deuxième fois, je finis avec juste "gg".

Vous aurez besoin quelque chose comme une fonction:

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 

Et puis utiliser que dans la boucle comme

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

Mais, comme je l'ai dit, le nombre d'occurrences par lui-même ne suffit pas à prouver la résiliation. Vous pouvez utiliser n'importe quel calcul comme mesure de résiliation. Tant qu'il diminue dans chaque itération de boucle et n'a pas de chaînes descendantes infinies.