なぜcoqでスクリプトを生成したのかを証明する方法は？

Question

私はframa-C WPを使用し、ACSLアノテーションをデバッグしたいと思います。 緑色またはオレンジ色の結果があります。私はなぜIDE3を開き、生成されたスクリプトを参照してください。その後、リストから理論/目標を選択し、Alt-ErgoまたはCoq IDEを起動することができます。私はCoq IDEで生成されたコードで遊びたいです。私は、例えば、その後、その後、定理WP いくつかの公理を見て：

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仕様のプログラムを持っているかを理解する良い方法はありますか？

Answer 1

Coqの「不完全なプルーフを保存しようとしました」はFrama-C/WPの「Unknown」によって変換されます。実際、Frama-Cは、intros ...とQedの間で対話的に証明を完了するのを待っています。 Coqを幸せにすることに成功した場合、スクリプトを保存すると、緑色（または黄色の緑色）の弾丸（「証明済み」）を持つことができます。

第2の質問については、対話形式でプルーフを実行しようとすると、問題がどこにあるのかを理解する良い方法です。 Coqとは別に、Why3（私が正しく思い出すならIsabelleとPVS）とWP、TIP（the WP manualのセクション2.3を参照）で直接構築された新しい対話型証明書で知られている対話式証明書を使用することができます。