在Dafny中查找和替換搜索和替換？

Question

我編碼a search and replace method，它使用查找，刪除和插入方法。我在一段時間內調用了這三種方法，我不確定我應該使用哪些前提條件。任何幫助，將不勝感激。

全碼：

 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

這是一個相當困難的事情來證明。這裏有一些最初的想法，這可能會對你有所幫助。

您需要找到循環的終止測量。我會建議使用類似於模式出現次數的元組以及字符串的長度。

您必須非常小心，替換不包含搜索詞，否則您的循環可能不會終止。即使它終止了，它也很難找到一個在每次迭代中都會減少的終止措施。例如，假設我想在字符串「ffggff」中用「gg」代替「fggf」，第一次循環我將有1次出現「fggf」，用「gg替換」fggf「 「結果在」fggf「 - 所以我仍然有一次發生！第二次我以「gg」結束。

你需要的東西就像一個功能：

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 

，然後使用在循環一樣

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

但是，就像我說的，事件本身的數量是不夠的證明終止。您可以使用任何計算作爲終止措施。只要它在每個循環迭代中減少並且沒有無限下行鏈。