验证移动数组区域的 Dafny 方法

Question

我正在使用 Dafny 在您收到的地方创建一个删除方法：

• 字符数组line

• 数组长度l

• 一个职位at

• 要删除的字符数p

首先删除at到at + p的行字符，然后必须将at + p右边的所有字符移动到at。

例如，如果你有[e][s][p][e][r][m][a]、at = 3、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;
  }
}

Here is the program on rise4fun

Answer 1

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

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

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

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

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

Extended solution on rise4fun.