1

私は Dafny を使用して、あなたが受け取る削除メソッドを作成しています:

  • 文字配列line

  • 配列の長さl

  • 位置at

  • 削除する文字数p

最初に at から to までの行の文字を削除し、次にtoat + pの右側のすべての文字を移動する必要があります。at + pat

たとえば、[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 は 2 つのエラーを出力します。

範囲外のインデックス 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

このような事後条件を表現するために量指定子を使用する必要はないと思います。それらは通常、配列をシーケンスにスライスすることでより適切に表現されます。

ループを検証しようとしているときは、ループ条件の否定と組み合わせたときに事後条件を暗示するのに十分強いループ不変条件を提供する必要があります。

ループ不変条件を選択するための適切な戦略は、postcondition メソッドを使用することですが、配列の長さをループ インデックスに置き換えます。

誘導が機能するには、ループ不変条件も十分に強力である必要があります。この場合、ループが行をどのように変更するかだけでなく、各反復で行のどの部分が同じままであるかを示す必要があります。

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 に答える