在 Dafny 中寻找 Search and Replace 的终止措施？

Question

我正在编写 a search and replace method 使用查找、删除和插入方法的代码。我在 while 循环中调用这三个方法，我不确定应该使用哪些先决条件。

完整代码：

      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" ，并将 "fggf" 替换为 "gg" 结果是 "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;
   }

但是，就像我说的，出现的次数本身并不足以证明终止。您可以使用任何计算作为终止措施。只要它在每次循环迭代中递减，并且没有无限递减链。

在 Dafny 中寻找 Search and Replace 的终止措施？

Finding a termination measure for Search and Replace in Dafny?

formal-verification

dafny