Dafnyメソッドは、逆の文字配列を返します

Question

文字の入力配列を取り、入力配列からなる別の配列を逆順に出力するメソッドを実装したいと思います。 1つのインデックス範囲6の外

predicate reversed (arr : array<char>, outarr: array<char>) 
requires arr != null && outarr != null 
//requires 0<=k<=arr.Length-1 
reads arr, outarr 
{ 
    forall k :: 0<=k<=arr.Length-1 ==> outarr[k] == arr[(arr.Length-1-k)] 
} 

method yarra(arr : array<char>) returns (outarr : array<char>) 
requires arr != null && arr.Length > 0 
ensures outarr != null && reversed(arr,outarr) 
{ 
    var i:= 0; 
    var j:= arr.Length-1; 
    outarr := new char[arr.Length]; 
    outarr[0] := arr[j]; 
    i := i+1; 
    j := j-1; 
    while i<arr.Length && 0<=j<arr.Length 
    invariant 0<=i<=arr.Length 
    decreases arr.Length-i, j 
    { 
    outarr[i] := arr[j]; 
    i:=i+1; 
    j:=j-1; 
    } 
    //return outarr; 
} 

method Main() 
{ 
    var s := ['a','b','a','b','a','b','a','b','a','b','a','b']; 
    var a,b,c,d := new char[5], new char[5], new char[5], new char[5]; 
    a[0], a[1], a[2], a[3], a[4] := 'y', 'a', 'r', 'r', 'a'; 
    d[0], d[1], d[2], d[3], d[4] := 'y', 'a', 'r', 'r', 'a'; 
    b := yarra(a); 
    c := yarra(b); 
    assert c[..] == a[..]; 
    //assert c.Length > -2; 
    //assert d[0] == a[0]; 
    //print c; print a; 
} 

1. エラー：私のコードしかし、私はエラー「私たちの範囲のインデックス」と私はここで

   が起こる何見当がつかない を「事後条件が成り立たない可能性があります」だです43

2. エラー2この戻りパスで事後条件が成立しないことがあります。 21 2

3. これは保持できない事後条件です。 13 26

   stdin.dfy（6,43）：エラー：インデックスが範囲外
   stdin.dfy（21,2）：エラーBP5003：事後条件が、このリターンパスに保持していないかもしれません。
   stdin.dfy（13,26）：関連する場所：これは保持できない可能性のある事後条件です。
   stdin.dfy（6,2）：関連場所
   stdin.dfy（6,47）：関連場所

Answer 1

Hereを確認し、あなたのプログラムのバージョンです。

解決するいくつかの問題がありました。

最初に、Dafnyがアクセスを見ることができないため、reversedの定義が不正です。outarr[k]が境界にあります。私は前提条件arr.Length == outarr.Lengthをreversedに加えることでこれを解決しました。

次に、reversedが呼び出される場所であれば、その新しい前提条件を考慮する必要があります。そのような場所はyarraの事後条件にありますが、私は追加の事後条件arr.Length == outarr.Lengthを追加して修正しました。

次に、ダフニーは、約reversedの事後条件がyarraに成立しないことがあると訴えています。これには、ループ不変量を強化する必要があります。これは、各インデックスについて順番に配列を配列することによって、配列のすべてのインデックスについて何かを証明しようとしている典型的なケースです。このような状況では、正しいループ不変式は「私は現在のインデックスよりも小さいすべてのインデックスでそれを確立しました」です。正しい不変であるので、我々は、このループ内で確立している事は、そのoutarr[k] == arr[arr.Length-1-k]です：これが通過するため

forall k | 0 <= k < i :: outarr[k] == arr[arr.Length-1-k] 

は最後に、我々は不変j == arr.Length - 1 - iを必要としています。 （実際、この不変量は、jを完全に取り除くことができたことを意味しますが、私は気にしませんでした。）