如何在coq中證明why3生成的腳本？

Question

我使用frama-C WP並希望調試我的ACSL註釋（瞭解爲什麼證明者說我「不知道」）。 我有一些綠色或橙色的結果。我打開why3 IDE並查看生成的腳本。然後我從列表中選擇一個理論/目標，並能夠啓動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. 

當我「走到底」的勒柯克，我看到一個錯誤「爲了挽救一個不完整的證據」。如何在Coq IDE中獲得「Proved」或「Unknown」的結果，我在frama-c或why3結果窗口中看到？ 還有什麼更好的方法來理解爲什麼我從證明者那裏得到了「我不知道」的信息，並決定我是否有一個錯誤或ACSL規範不好的程序？

Answer 1

在Coq中的「試圖保存不完整的證據」在Frama-C/WP中被翻譯爲「未知」。事實上，Frama-C正在等待您交互式地完成intros ...與Qed之間的證明。如果成功使Coq快樂，則保存腳本將允許您使用綠色（或黃綠色）子彈（「證明」）。

關於你的第二個問題，試圖交互式地進行證明是一個很好的方法來理解問題在哪裏。除Coq外，您可以使用Why3（Isabelle和PVS，如果我正確記得的話）已知的交互式證明器，以及直接在WP，TIP中建立的新交互式證明器（請參閱the WP manual的第2.3節）。