Dafny: Fail to verify full string by adding characters to string

Question

method AddCharsToString(str: string, len: int, c: char) returns (res: string)
  requires 0 <= len
  ensures |res| == len+|str|
  ensures forall j :: 0 <= j < len ==> res[j] == c
  ensures forall k :: 0 <= k < |str| ==> res[k+len] == str[k]
{
  var left := len;
  var i := 0;
  res := str;
  while i < left
    decreases left - i
    invariant 0 <= i <= left
    invariant |res| == |str| + i
    invariant forall j :: 0 <= j < i ==> res[j] == c
    invariant forall k :: 0 <= k < |str| ==> res[i+k] == str[k]
  {
    res := [c] + res;
    i := i + 1;
  }

}
method Main() {
  var stringOne := "foo";
  var test:= AddCharsToString(stringOne, 2, '0');

  //assert test == ['0', '0']+['f','o','o'];
  assert test == ['0', '0', 'f', 'o', 'o'];
}

method AddCharsToString verify assert of full string, only if the frist assert is verified. Why is it not enough to say that my method verify test == ['0', '0', 'f', 'o', 'o']?

method AddCharToString (str: string, c: char ) returns (res: string)
  ensures |res| == 1+|str|
  ensures res == [c]+str
  ensures forall i :: 0 <= i <= 0 ==> res[i] == c
  ensures forall i :: 0 <= i < |str| ==> res[i+1] == str[i]
{
  res := [c]+ str ;
}

method Main() {
  var stringOne := "foo";
  var test_two := AddCharToString(stringOne, '0');

  //assert test_two == ['0']+['f','o','o'];
  assert test_two == ['0','f','o','o'];
}

If only character is added to the string then there is no problem, because ensures res == [c]+str.

Answer 1

Sometimes, the verifier cannot complete the proof by itself, but needs more help from the user. Your example is such an example.

In your case, the issue is that the verifier doesn't figure out how to instantiate the last postcondition of AddCharsToString. In Main, you're trying to prove something about test[i] (for all i), which requires instantiating the quantifier with k := i - len. Evidently, the verifier wasn't creative enough to come up with this instantiation.

If you instead rewrite the last postcondition into

  ensures forall k :: len <= k < |res| ==> res[k] == str[k-len]

then it's "more obvious" to the verifier how to instantiate the quantifier to get some information about res[i], namely k := i.

A different way to get the proof to go through is to change the last postcondition to

  ensures res[len..] == str

If you do that, you may also consider changing the last loop invariant to

    invariant res[i..] == str