1

我正在使用 Dafny 制作一个删除方法，您会收到：

  • 字符数组line

  • 数组的长度l

  • 一个位置at

  • 要删除的字符数p

首先从 at to 删除 line 的字符at + p，然后必须移动at + pto右边的所有字符at。

例如，如果您有[e][s][p][e][r][m][a], and at = 3, and p = 3, 那么最终结果应该是[e][s][p][a]

我试图证明一个有意义的后置条件，例如：

ensures forall j :: (at<=j<l) ==> line[j] == old(line[j+p]);

确保 at + p 右侧的所有字符都在新位置。

但是 Dafny 输出两个错误：

索引超出范围 7 53

后置条件可能不会在此返回路径上成立。19 2

method delete(line:array<char>, l:int, at:int, p:int)
  requires line!=null;
  requires 0 <= l <= line.Length && p >= 0 && at >= 0;
  requires 0 <= at+p <= l;
  modifies line;
  ensures forall j :: (at<=j<l) ==> line[j] == old(line[j+p]) ; 
{
  var tempAt:int := at;
  var tempAt2:int := at;
  var tempPos:int := at+p;
  while(tempAt < at + p)
    invariant at<=tempAt<=at + p;
  { 
    line[tempAt] := ' ';
    tempAt := tempAt + 1;
  }

  while(tempPos < line.Length && tempAt2 < at + p)
    invariant at + p<=tempPos<=line.Length;
    invariant at<=tempAt2<=at+p;
  {
    line[tempAt2] := line[tempPos];
    tempAt2 := tempAt2 + 1; 
    line[tempPos] := ' ';
    tempPos := tempPos + 1;
  }
}

这是rise4fun上的程序

4

1 回答 1

1

我认为没有必要使用量词来表达这样的后置条件。它们通常通过将数组分割成序列来更好地表达。

当您尝试验证循环时，您需要提供一个足够强大的循环不变量，以在与循环条件的否定相结合时暗示后置条件。

选择循环不变量的一个好策略是使用方法后置条件，但用循环索引替换数组长度。

您的循环不变量还需要足够强大才能使归纳起作用。在这种情况下，您不仅需要说明循环如何修改 line，还需要说明 line 的哪些部分在每次迭代中保持不变。

rise4fun 上的解决方案。

// line contains string of length l
// delete p chars starting from position at
method delete(line:array<char>, l:nat, at:nat, p:nat)
  requires line!=null
  requires l <= line.Length
  requires at+p <= l
  modifies line
  ensures line[..at] == old(line[..at])
  ensures line[at..l-p] == old(line[at+p..l])
{
  var i:nat := 0;
  while(i < l-(at+p))
    invariant i <= l-(at+p)
    invariant at+p+i >= at+i 
    invariant line[..at] == old(line[..at])
    invariant line[at..at+i] == old(line[at+p..at+p+i])
    invariant line[at+i..l] == old(line[at+i..l]) // future is untouched
  { 
    line[at+i] := line[at+p+i];
    i := i+1;
  }
}

用空格覆盖

如果你想用空格覆盖旧字符串的尾随部分，你可以这样做：

method delete(line:array<char>, l:nat, at:nat, p:nat)
  requires line!=null
  requires l <= line.Length
  requires at+p <= l
  modifies line
  ensures line[..at] == old(line[..at])
  ensures line[at..l-p] == old(line[at+p..l])
  ensures forall i :: l-p <= i < l ==> line[i] == ' '  
{
  var i:nat := 0;
  while(i < l-(at+p))
    invariant i <= l-(at+p)
    invariant at+p+i >= at+i 
    invariant line[..at] == old(line[..at])
    invariant line[at..at+i] == old(line[at+p..at+p+i])
    invariant line[at+i..l] == old(line[at+i..l]) // future is untouched
  { 
    line[at+i] := line[at+p+i];
    i := i+1;
  }

  var j:nat := l-p;
  while(j < l)
    invariant l-p <= j <= l
    invariant line[..at] == old(line[..at])
    invariant line[at..l-p] == old(line[at+p..l])
    invariant forall i :: l-p <= i < j ==> line[i] == ' '
  {
    line[j] := ' ';
    j := j+1;
  }
}

rise4fun 上的扩展解决方案。

于 2016-04-14T14:04:37.597 回答