Dafny挿入メソッドで、この戻りパスで事後条件が成立しない可能性があります

Question

長さ「l」の文字列と長さ「ll」の文字列を含む配列「nl」を含む配列「line」を持っています"p"。 注： "l"と "p"は必ずしも対応する配列の長さである必要はありません。パラメータ "at"は "line"内に挿入される位置になります。 再開：長さ「p」の配列が「行」に挿入され、位置（at、i、at + p）、「p」位置の間の「行」のすべての文字が右に移動して挿入されます。

私の論理は、「行」に挿入された要素の順序が同じで、「nl」に含まれる文字と同じ順序であるかどうかを確認することです。ここで

はthe codeです：ここでは

method insert(line:array<char>, l:int, nl:array<char>, p:int, at:int) 
    requires line != null && nl != null; 
    requires 0 <= l+p <= line.Length && 0 <= p <= nl.Length ; 
    requires 0 <= at <= l; 
    modifies line; 
    ensures forall i :: (0<=i<p) ==> line[at+i] == nl[i]; // error 
{ 
    var i:int := 0; 
    var positionAt:int := at; 
    while(i<l && positionAt < l) 
    invariant 0<=i<l+1; 
    invariant at<=positionAt<=l; 
    { 
    line[positionAt+p] := line[positionAt]; 
    line[positionAt] := ' '; 
    positionAt := positionAt + 1; 
    i := i + 1; 
    } 

    positionAt := at; 
    i := 0; 
    while(i<p && positionAt < l) 
    invariant 0<=i<=p; 
    invariant at<=positionAt<=l; 
    { 
    line[positionAt] := nl[i]; 
    positionAt := positionAt + 1; 
    i := i + 1; 
    } 
} 

は、私が受けていerrorsです。

ありがとうございました。

Answer 1

私はそれを考慮にp場所によって位置atで始まる文字をシフトするline内の文字列の末尾の上にそれらを記述するかもしれないという事実を取るようには見えないので、あなたのアルゴリズムは、正しくないと思われます。

私の経験では、順番にコード開発の検証

1. グッド基準に成功するためにということであったが不可欠です。変数の名前の変更、コードの書式設定、およびその他のコード規則は、通常よりもより重要です。
2. 論理的にシンプルなコードを書くことは本当に役に立ちます。余分な余分な変数を避けるようにしてください。実用的なところでは、算術式と論理式を単純化してみてください。
3. 正しいアルゴリズムから始めると、検証が容易になります。もちろん、これは完了したよりも簡単です！
4. 考えられる最も強いループ不変量を書くことは、しばしば役に立ちます。
5. 事後条件から後ろ向きに作業することは、しばしば役に立ちます。あなたのケースでは、事後条件と最終ループ条件の否定を取り、後条件を暗示するために最終ループの不変量がどのようなものでなければならないかを調べるためにこれらを使用します。
6. 配列を操作するとき、配列の元の値を含むゴースト変数をシーケンスとして使用することは、しばしば効果的な戦略です。ゴースト変数はコンパイラの出力には表示されないので、プログラムのパフォーマンスには影響しません。
7. 事後条件がより弱い性質を必要とするだけであっても、アレイの正確な状態のアサーションを書き留めることは、しばしば有用です。ここで

ご希望の手順の検証実装です：あなたはそれのために利用可能である場合に

// l is length of the string in line 
// p is length of the string in nl 
// at is the position to insert nl into line 
method insert(line:array<char>, l:int, nl:array<char>, p:int, at:int) 
    requires line != null && nl != null 
    requires 0 <= l+p <= line.Length // line has enough space 
    requires 0 <= p <= nl.Length // string in nl is shorter than nl 
    requires 0 <= at <= l // insert position within line 
    modifies line 
    ensures forall i :: (0<=i<p) ==> line[at+i] == nl[i] // ok now 
{ 
    ghost var initialLine := line[..]; 

    // first we need to move the characters to the right 
    var i:int := l; 
    while(i>at) 
    invariant line[0..i] == initialLine[0..i] 
    invariant line[i+p..l+p] == initialLine[i..l] 
    invariant at<=i<=l 
    { 
    i := i - 1; 
    line[i+p] := line[i]; 
    } 

    assert line[0..at] == initialLine[0..at]; 
    assert line[at+p..l+p] == initialLine[at..l]; 

    i := 0; 
    while(i<p) 
    invariant 0<=i<=p 
    invariant line[0..at] == initialLine[0..at] 
    invariant line[at..at+i] == nl[0..i] 
    invariant line[at+p..l+p] == initialLine[at..l] 
    { 
    line[at + i] := nl[i]; 
    i := i + 1; 
    } 

    assert line[0..at] == initialLine[0..at]; 
    assert line[at..at+p] == nl[0..p]; 
    assert line[at+p..l+p] == initialLine[at..l]; 
} 

http://rise4fun.com/Dafny/ZoCv