验证移动数组区域的 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 输出了两个错误：

index out of range 7 53

postcondition might not hold on this return path. 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

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

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

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

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

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.

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

Verifying a Dafny method that shifts a region of an array

formal-verification

induction

dafny