問題タブ [why3]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
frama-c - Frama-C GUI で Why3 証明を使用するには?
これはばかげた質問のように感じますが、困惑しています。Frama-C Sodium と Why3 0.86.1 (両方とも OPAM 経由でインストール) を使用して、単純なプロパティを証明しようとしています。このプログラムを考えてみましょう ( toy.c):
Frama-C GUI と Why3 を使用して、この主張を証明したいと思います。だから私は実行frama-c-gui toy.cし、証明者として「Why3（ide）」を選択し、メイン関数で「WPによる関数注釈の証明」を実行します。(または、「WP の目標」タブに移動し、そこから Why3 IDE を実行します。) Why3 が表示されたら、選択した証明者を呼び出してすべてを緑色に変更し、セッションを保存して Why3 を終了しますが、Frama では何も起こりません。 -C GUI: プロパティはまだオレンジ/「確認しようとしましたが、決定できませんでした」とマークされています。
Why3 によって生成された証明を実際に使用するように Frama-C に指示するにはどうすればよいですか? 証明自体は間違いなくそこにあります。Why3 をもう一度開いても、すべてが緑色のままなので、セッションは適切に保存されています。また、Frama-C は何かが起こったことを認識しています。Why3 IDE が開いている間、小さな歯車の記号が WP の目標タブに表示され、Why3 を閉じると消えます。
(この特定の特性は、Why3 を使用しなくても Alt-Ergo で証明できることはわかっていますが、より難しい問題には Why3 が必要です。)
why3 - 長さがゼロの場合の array_eq_sub の動作
に次の補題がありますwhy3。
これは基本的なケースの動作のようですが、明らかにそうではありません。これが機能しない理由についてのアイデアはありますか?
更新
私は問題を単一の不足している補題に減らすことができました:
ドキュメントarray_eq_subで指定されている の定義を考えると、これも些細なことのようです。証明者が解決策を見つけられないのはなぜですか?
frama-c - MacOS で FromInt.v のコンパイルが失敗する (Coq で wp プラグインを使用しようとしている)
私が試してみると：
次に、次のエラーが表示されます。
(FromInt.v より前の他のすべてのファイルは正常にコンパイルされているようです)。この動作は、opam を介して why3 および frama-c パッケージをアンインストールして再インストールした後でも持続します。
これを修正する方法を知っている人はいますか？
MacOS High Sierra を使用しています。関連するバージョン情報: Why3 プラットフォーム、バージョン 0.88.3、OCaml トップレベル、バージョン 4.05.0、Frama-C Phosphorus-20170501c02v53d5hv2r、および Coq Proof Assistant、バージョン 8.7.0 (2017 年 12 月)、すべて opam を介してインストールされます。