Dafny：无法通过向字符串添加字符来验证完整字符串

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

方法 AddCharsToString 验证完整字符串的断言，仅当第一个断言被验证时。 为什么仅仅说我的方法验证测试 == ['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'];
}

如果只向字符串添加字符则没有问题，因为确保 res == [c]+str.

Answer 1

有时候，验证者自己无法完成证明，需要用户更多的帮助。你的例子就是这样的例子。

在你的情况下，问题是验证者没有弄清楚如何实例化

AddCharsToString

的最后一个后置条件。在

Main

中，您试图证明关于

test[i]

（对于所有

i

）的一些事情，这需要用

k := i - len

实例化量词。显然，验证者没有足够的创造力来想出这个实例。

如果你改为将最后一个后置条件重写为

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

那么对于验证者来说“更明显”的是如何实例化量词来获取一些关于

res[i]

的信息，即

k := i

.

获得证明的另一种方法是将最后一个后置条件更改为

  ensures res[len..] == str

如果你这样做，你也可以考虑将最后一个循环不变量更改为

    invariant res[i..] == str