問題タブ [dafny]

このプログラムを dafny で証明しようとしていますが、最後の不変条件でエラーが発生し、なぜ機能しないのかわかりません。

このプログラムは、ソートされた配列に int を挿入するメソッドで構成されています。int は正しい位置に挿入されます。つまり、5 を 1,2,3,4,5,6,7 に挿入すると、次の値が返されます: 1,2,3,4,5,5,6,7

ありがとう

ここで何が問題なのか誰でも助けてくれますか。このプログラムを検証すると、以下のエラーが発生します。

いろいろ試してみましたが、検証に合格しません。助けてください。

…………

私は Dafny でのレンマの使用を見てきましたが、理解するのが難しいと感じており、明らかに以下の例は検証されていません。これはおそらく、Dafny が帰納法またはカウントのいくつかのプロパティを証明するためのレンマのようなものを見ていないためです。 ? 基本的に、カウントが帰納的であるなどのことを Dafny に納得させるために、何をどのように定義する必要があるのか​​ わかりません。保証と不変条件の仕様の一部は必要ありませんが、それは重要ではありません。ところで、これは Spec# の方が簡単でした。

オフィスからの問題 - ツリーの最前線は、左から右へのチップ値のシーケンスです。次の IO クラスの OUTPUT メソッドを使用して、特定のツリーの最前線を出力する反復コードを開発する必要があります。

line長さ の文字列が含まれる配列があります。これはl、 pat長さ の文字列が含まれる別の配列ですp。注:pとlは配列の長さではありません

目的は、に含まれる文字列が にpat存在するかどうかを確認することですline。その場合、このメソッドはline単語の最初の文字のインデックスを返し、そうでない場合は を返す必要があり-1ます。

「トリガーする用語が見つかりません」というエラーを引き起こしている不変条件はensures exists j :: ( 0<= j < l) && j == pos;、invariant forall j :: 0 <= j < iline ==> j != pos;

ループの私の論理は、それらがループ内にある間、インデックスが見つからなかったということです。そして、確実なのは、インデックスに遭遇したときです。

何が間違っている可能性がありますか？

コードは次のとおりです。

次のエラーが表示されます: Dafny 出力のスクリーンショット

これが rise4funのコードです。

長さ「l」の文字列が含まれる配列「line」と、長さ「p」の文字列が含まれる配列「nl」があります。注: "l" と "p" は、対応する各配列の長さである必要はありません。パラメーター "at" は、挿入が "line" 内で行われる位置になります。再開: 長さ "p" の配列が "line" に挿入され、位置 (at,i,at+p),'p' の位置の間で "line" のすべての文字が右に移動して挿入されます。

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

コードは次のとおりです。

これが私が受け取っている エラーです。

ありがとう。

特定の Dafny プログラムが検証するかどうかを問い合わせたいと思います。Dafny は通常、Visual Studio IDE 内でインタラクティブな方法でプログラムを開発するために使用されます。

ただし、非対話的な方法でクエリを実行する必要があります。特に、Python プログラム内から Dafny にクエリを実行する必要があります。これは可能ですか？

私は 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

rise4funのプログラムはこちら

次のプログラムでエラーが発生する理由を知りたいです。

私が得た：invalid UnaryExpressionこれを実行したとき。