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

但是，就像我说的，事件本身的数量是不够的证明终止。您可以使用任何计算作为终止措施。只要它在每个循环迭代中减少并且没有无限下行链。