insert - Dafny 插入方法，后置条件可能不会在此返回路径上成立

Question

我有一个数组“line”，其中包含一个长度为“l”的字符串，还有一个数组“nl”，其中包含一个长度为“p”的字符串。 注意:“l”和“p”不一定是每个对应数组的长度。参数“at”将是在“line”内插入的位置。 继续:长度为“p”的数组将被插入到“line”中，将位置(at，i，at + p)，'p'位置之间的“line”的所有字符向右移动以便进行插入。

我的确保逻辑是检查“line”中插入的元素是否具有相同的顺序并且与“nl”中包含的字符相同。

这里是the code :

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 && 0 <= p <= nl.Length ;
  requires 0 <= at <= l;
  modifies line;
  ensures forall i :: (0<=i<p) ==> line[at+i] == nl[i]; // error
{
  var i:int := 0;
  var positionAt:int := at;
  while(i<l && positionAt < l)
    invariant 0<=i<l+1;
    invariant at<=positionAt<=l;
  {
    line[positionAt+p] := line[positionAt];
    line[positionAt] := ' ';
    positionAt := positionAt + 1;
    i := i + 1;
  }

  positionAt := at;
  i := 0;
  while(i<p && positionAt < l)
    invariant 0<=i<=p;
    invariant at<=positionAt<=l;
  {
    line[positionAt] := nl[i];
    positionAt := positionAt + 1;
    i := i + 1;
  }
}

这里是errors 我收到了。

谢谢。

Answer 1

我怀疑您的算法不正确，因为它似乎没有考虑到将从位置 at 开始的字符移动到 p 位置可能会写成它们位于 line 中字符串的末尾。

我的经验是，为了成功验证

1. 良好的代码开发标准至关重要。良好的变量命名、代码格式和其他代码约定比平常更重要。
2. 编写逻辑简单的代码确实很有帮助。尽量避免无关的额外变量。尽可能简化算术和逻辑表达式。
3. 从正确的算法开始可以使验证更容易。当然，说起来容易做起来难!
4. 写出您能想到的最强的循环不变量通常会很有帮助。
5. 从后置条件逆向工作通常很有帮助。在您的情况下，采用后置条件和最终循环条件的否定 - 并使用它们来计算出最终循环的不变量必须是什么，以便暗示后置条件。然后从该循环向后工作到上一个循环，等等
6. 在操作数组时，使用包含数组原始值作为序列的幽灵变量通常是一种有效的策略。幽灵变量不会出现在编译器输出中，因此不会影响程序的性能。
7. 写下数组的确切状态的断言通常很有帮助，即使后置条件只需要一些较弱的属性。

这是您所需过程的经过验证的实现:

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

http://rise4fun.com/Dafny/ZoCv