Finding a termination measure for Search and Replace in Dafny?

Question

I'm coding a search and replace method that uses find, delete and insert methods. I'm calling these three methods inside a while loop and I'm not sure about which pre-conditions should I use.

Full 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

This is a fairly difficult thing to prove. Here are some initial ideas, which might help you.

You need to find a termination measure for the loop. I would suggest using something like a tuple of the number of occurrences of the pattern, and the length of the string.

You must be very careful that the replacement doesn't contain the search term, otherwise your loop may not terminate. And even if it does terminate, its hard to find a termination measure that will reduce at each iteration.

For example, say I want to replace "fggf" with "gg" in the string "ffggff", the first time round the loop I will have 1 occurrence of "fggf", and replacing "fggf" with "gg" results in "fggf" - so I still have one occurrence! The second time round I end up with just "gg".

You will need something like a function:

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

And then use that in the loop like

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

But, like I said, the number of occurrences by itself is not enough to prove termination. You can use any calculation as the termination measure. As long as it decrease in each loop iteration and has no infinite descending chains.