如何在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节）。