問題タブ [hoare-logic]

これはアルゴリズムです：

私はいくつかの調査を行い、不変条件を に絞り込みましたif x is in a[0 .. n-1] then a[l] <= x < a[r]。

私はそこからどのように進歩するのか分かりません。前提条件が広すぎるようで、それを示すのに苦労していP -> Iます。

どんな助けでも大歓迎です。これらは、アルゴリズムの正しさを証明するために使用できる論理規則です。

事後条件: Q = {0 <= x <= 15}

正しい事前条件 P1 = {-1 <= x} または P2 = {0 <= x <= 15}

そして、どうすればそれを計算できますか？

配列セル内の各桁の表現に 2 つの long 整数を追加する (WP ループの不変条件を調べるための) テスト コードがあります。

最後のループの不変条件のみを指定したい。\at(a[i], LoopCurrent) を使用して ACSL コードをいくつか試しました。不明なステータスまたはタイムアウトを受け取りました。最後に、成功せずに公理的再帰ソリューションを終了しました。

これを確認するために他に何を試みるべきか、今のところわかりません。ヘルプ？

更新: 実際の計算用の関数を作成しました。改善された公理。まだタイムアウトステータスを取得しています。opam の Frama-C 最新リリースをデフォルト設定 (タイムアウト = 10、証明者 Alt-Ergo) で実行しました。