Dafny 插入方法，此 return 路径上可能没有后置条件

Question

我有一个数组 "line"，其中包含一个长度为 "l" 的字符串，还有一个数组 "nl"，其中包含一个长度为 "p" 的字符串. 注意："l" 和 "p" 不一定是每个对应的长度 array.The 参数 "at" 将在 [=24= 内进行插入的位置]. 恢复：长度为"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.

中的字符串

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

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

这是您所需程序的经过验证的实施：

// 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

Dafny 插入方法，此 return 路径上可能没有后置条件

Dafny insert method, a postcondition might not hold on this return path

insert

induction

formal-verification

loop-invariant

dafny