私はframa-C WPを使用し、ACSLアノテーションをデバッグしたいと思います。 緑色またはオレンジ色の結果があります。私はなぜIDE3を開き、生成されたスクリプトを参照してください。その後、リストから理論/目標を選択し、Alt-ErgoまたはCoq IDEを起動することができます。私はCoq IDEで生成されたコードで遊びたいです。私は、例えば、その後、その後、定理WP いくつかの公理を見て:なぜcoqでスクリプトを生成したのかを証明する方法は?
intros a a_1 i_3 i_2 i_1 i t_2 t_1 t t_8 t_7 t_6 t_5 t_4 t_3 a_4 a_3 a_2 x
x_1 x_2 x_3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18
h19 h20 h21 h22 h23 h24 h25.
Qed.
私はコックに「最後に移動」するとき、私はエラーが「不完全な証拠を保存しよう」を参照してください。私はframa-cまたはwhy3結果ウィンドウに表示されるCoq IDEで "Proved"または "Unknown"の結果をどのように得ることができますか? そして、どうして私が証明者からのメッセージを "私は知らない"と思って、バグのあるプログラムか悪いACSL仕様のプログラムを持っているかを理解する良い方法はありますか?
CoqをWhy3から呼び出すことも、Frama-Cから直接呼び出すこともできます。 – eponier