Dafny: is recursive function enough to verify iterative find-and-replace?

Question

In Dafny, I'm working with an iterative approach to find all instances of a given substring and replace them with another given substring.

method findAndReplace(str:string, toFind:string, toReplace:string) returns (newString:string)
    requires |toFind| > 0
    ensures newString == verify(str, toFind, toReplace)
    {
        newString := "";
        var i := 0;
        while (i < |str|) 
        invariant i <= |str|
        invariant newString == verify(str[..i], toFind, toReplace) // flagged as not maintained by loop 
        decreases |str| - i
        {
            if( toFind <= str[i..]) {
                newString := newString + toReplace;
                i := i + |toFind|;
            }
            else {
                var next := str[i..i+1];
                newString := newString + next;
                i := i + 1;
            }
        }
        return newString;
    }

Included in the ensures and invariant is a call to a function verify meant to help verification along.

    function verify(str:string, toFind:string, toReplace:string) : string 
    requires |toFind| > 0
    decreases str
    {
        if |str| < |toFind| 
        then
            str 
        else 
            if str[..|toFind|] == toFind 
            then
                toReplace + verify(str[|toFind|..], toFind, toReplace)
            else
                str[..1] + verify(str[1..], toFind, toReplace)
    }

Except it doesn't verify. Specifically, the invariant is flagged as not maintained by the loop.

My question is this: Is it due to difference in control flow between the iterative method and the recursive function that dafny is unable to connect them? If I were to somehow come up with an iterative function that does practically the same thing as verify, would dafny have an easier time verifying the invariant?

What really makes me think this is the case is because I have a recursive method that works just fine with verify

    method findAndReplace(str : string, toFind : string, toReplace : string) returns (newString : string)
    requires |toFind| > 0
    ensures newString == verify(str, toFind, toReplace)
    decreases str
    {
        if (|str| < |toFind|)
        {
            return str;
        }

        if (toFind <= str)
        {
            var result := findAndReplace(str[|toFind|..], toFind, toReplace);
            return toReplace + result;
        }
        else
        {
            var result := findAndReplace(str[1..], toFind, toReplace);
            return str[..1] + result;
        }
        
    }

It seems like its important that a method and its corresponding function should follow the same basic structure for easier verification, but I couldn't find any such imperative in the dafny docs. The other part of me says as long as they give identical output on any input, dafny should see their behavior as identical.

Answer 1

Having spent quite a while on this problem, it does seem to be quite tricky. The issue is that the direction of recursion appears to "naturally" go against the direction of iteration. Specifically:

• (findAndReplace) Here, you append onto the end of newString.

• (verify) Here, you append onto the beginning of the string.

For some problems, its relatively easy to rework the recursion to go in the other direction. In this case, I didn't find an easy way to do it.

However, I did manage to prove a less powerful result which is perhaps a good step towards a final solution:

// Check whether string ends with a given ending.
function endsWith(str:string, end:string) : bool {
    var n := |str| - |end|;
    |str| >= |end| && str[n..] == end
}
// Extract last character from string
function last(str:string) : char
    requires |str| > 0 {
        str[|str|-1]
}
// Remove last n characters from string
function remove(str:string, n: int) : string
    requires 0 <= n <= |str| {
        str[..|str|-n]
}

function verify(str:string, nstr:string, toFind: string, toReplace: string) : bool
requires |toFind| > 0  {
  // Case one, a replace happened
  (endsWith(str,toFind) && endsWith(nstr,toReplace) && 
   verify(remove(str,|toFind|),remove(nstr,|toReplace|),toFind,toReplace)) ||
  // Case two, a replace did not happen
  (str != nstr ==> (|str| > 0 && |nstr| > 0 && last(str) == last(nstr) && 
   verify(remove(str,1),remove(nstr,1),toFind,toReplace)))
}

method findAndReplace(str:string, toFind:string, toReplace:string) returns (nstr:string)
requires |toFind| > 0
// ensures newString == verify(str, toFind, toReplace)
{
    nstr := "";
    var i := 0;
        
    while (i < |str|)
        invariant 0 <= i <= |str|
        invariant verify(str[..i],nstr,toFind,toReplace)
        decreases |str| - i
        {
            if toFind <= str[i..] {
                nstr := nstr + toReplace;
                i := i + |toFind|;
                // Make equivalence explicit.
                assert remove(str[..i],|toFind|) == str[..i-|toFind|];
            } else {
                var next := str[i..i+1];
                nstr := nstr + next;
                i := i + 1;
                // Make equivalence explicit.
                assert remove(str[..i],1) == str[..i-1];
            }
    }
    return nstr;
}

This is strictly less powerful because it doesn't specify the order of substitution. For example, replacing oo with tt in ooo is allowed to produce either tto or ott.