問題タブ [why3]

Windows（Cygwin）用のクラカトアとジェシー（why-2.33）でwhy3ide（why3-0.81）をコンパイルしようとしています。表記を表示するために右下のテキストボックスを作成できないことを除いて（常に空です）、すべてがうまくいきました。

画像: https://dl.dropboxusercontent.com/u/39984835/why3ide/error_capture.jpg

このエラーは次のとおりです。

このエラーをデバッグするにはどうすればよいですか? （私はOCamlの初心者です）

format.ml ファイルはこちら:
cygwin/lib/ocaml/format.ml

Introduction_Premises変換を参照するファイルは次の場所にあります:
why3-0.81/ drivers /
gappa.drv

PS この投稿にwhy3タグとwhy3ideタグを追加しようとしましたが、私の評判はまだ十分ではありません.

frama-c と why3 をインストールしましたが、frama-c を起動しようとすると、jessie3 でエラーが発生します。

camlGzip に関する情報が見つからないため、構成ファイル (camlzip である可能性があります) でエラーになる可能性がありますが、宣言されている場所はわかりません。

編集: Jessie3.cmxs の camlzip で camlGzip を変更しようとしましたが、frama-c を起動するとセグメンテーション違反が発生します

私のframa-cとWhy3のバージョン：

Mint17 仮想マシンで作業していますが、各プログラムの ./configure と make にエラーはありませんでした

誰かがすでにこの問題を抱えていて、私を助けてくれることを願っています

プログラムのバグを示すテスト ケースを導出するために使用できるモデルを取得するために、Why3 の Z3 バックエンドを使用しようとしています。ただし、Z3 バージョン 4.3.2 はsat、Why3 の目標に答えることができないようです。Why3 で使用されている公理的な定義の一部が Z3 を混乱させているようです。たとえば、次の例 (Why3 が生成するもののごく一部です)

timeout次のコマンドラインで結果が得られます。

一方、定義を次のように変更すると、

モデルを取得します（かなり妥当に見えます）

しかし、元のWhy3ファイルに存在する次の公理を追加しようとすると、つまり

再びZ3が答えますtimeout。

Z3 の設定で何か足りないものはありますか? さらに、Why3 の以前のバージョンには、MODEL_ON_TIMEOUTそのような状況でモデルを取得できるオプションがありました。Z3がチェックを終了できなかったため、これが実際のモデルであるという保証はありませんでしたが、実際には、そのようなモデルには通常、必要なすべての情報が含まれていました. ただし、4.3.2 には同様のオプションが見つかりませんでした。それはまだ存在しますか？

更新最後の公理Abs_posは間違っていました (ここに投稿する前に Why3 の出力を少しいじり、間違ったバージョンの問題を貼り付けてしまいました)。これは修正されました。

Windows環境でプラグインを介してcvc4証明者を使用しようとしています。システムにインストールしています。Why3 は、証明者として cvc4 を含めるように適切に構成されています。Frama-c wpWhy3frama-cwhy3

次のコマンドを使用して、frama-c Wp プラグインを使用して、.c ファイル (ACSL 仕様の C ソース ファイル) に対応する why3 形式 (.why) ファイルを生成しました。

上記のコマンドは、ディレクトリにファイルswap_Why3_ide.whyを生成しますC:/Users/user/temp/typed。

証明者と​​してwithをswap_Why3_ide.why使用して、生成されたファイルで Theories を証明しようとすると、次のエラーで失敗します。why3cvc4

Linux 環境で同じ手順を実行し、why3証明者を実行できました。

WindowsでWhy3を実行する方法を提案できる人はいますか?

こんにちは、自動控除と検証ハッカー！

WhyML が ACSL アノテーション付き C プログラムの証明をどのように正確に提供するかをより深く理解するために、Why3 が WhyML プログラムで行う作業を手動で「再現」し、それを SMT ロジックに変換して Z3 証明者にフィードしようとしています。

次の C フラグメントがあるとします。

次のように SMT ロジックにエンコードしようとしています。

Z3 は「不明」を返します。

これはおそらく、set_a_i 関数を指定する際に使用される数量化によるものです。しかし、それを指定する他の方法はありません。

私は次の声明を認識しています。

• 一般に、SMT ソルバーは、配列の数量化を処理できません (または悪い方法で処理します)。
• 事前条件と事後条件およびループ不変条件を指定すると、WhyML はそのようなプログラムを証明できます。
• バックエンドがZ3に設定されている場合でも、なぜMLはそのようなプログラムを証明できるので、SMTソルバー自体は問題になりません.
• WhyML は z3 smt ファイルを生成できますが、理由の 1 つは、WhyML から smt への変換が自動的に行われるため、それを理解するのは大変な労力です (たとえば、変数名を保持しません)。

WhyML、Frama-C WP プラグイン、Z3 について提供されたほぼすべての資料を読みました。また、C コードの検証に関するいくつかの論文を読みましたが、C --> SMT 変換技術に関するものは何も見つかりませんでした。

この理解を得るには、どの資料を学習すればよいですか? 命令型コードをマルチソートされた一次ロジックに変換するこの機構を説明している論文への洞察やリンクを提供していただけませんか。

コメントをいただければ幸いです。ありがとう！

がんばれ、エフゲニー。

次の注釈付き C コードがあるとします。

Z3 も Alt-ergo も、アサート final_a と事後条件を証明できません。Z3 はループ不変式も証明できません。

Alt-Ergo の出力:

Z3 の出力:

何が欠けている？

ACSL で定義された帰納述語で帰納を使用することは可能ですか?

ACSL マニュアルの次の例を検討してください。

次の補題を証明しようとしています。

Alt-Ergo はここで失敗するので、手動の Coq 推論に頼ります。

しかし、 Iの場合Search P_reachable、次の 2 つの公理のみが生成されていることがわかります。

そして誘導原理はありません。だから応募できないinduction P_reachableとかdestruct P_reachable。

frama-cバージョン Sodium-20150201の WP プラグインを使用しています。

再現するには、との定義と補題frama-c -wp -wp-rte -wp-prover coqide file.cがfile.c含まれているを実行できます。Listreachablenext_null_reachable