2

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

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

这是代码：

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

这是 我收到的错误。

谢谢。

4

1 回答 1

3

我怀疑你的算法是不正确的，因为它似乎没有考虑到这样一个事实，即从位置开始移动字符at可能p会将它们写在字符串的末尾line。

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

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

于 2016-04-06T08:57:52.320 回答