は、私はあなたが受け取るdeleteメソッドを作るためにDafnyを使用してい

Question

配列の領域にシフトしDafny方法の検証：

• char配列line

• 配列の長さl

• 位置at

• デルへの文字数ETE p

まず、あなたは、よりat + pに行の文字を削除してから、あなたはatにat + pの右側のすべての文字を移動する必要があります。

あなたが[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の右側のすべての文字が確実に新しい位置にあるようにする。このリターンパスに保持しない場合があります7 53

事後条件範囲外

が

インデックス：

しかしDafnyは、2つのエラーを出力します。 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.

を