如何在coq中证明why3生成的脚本？

Question

我使用frama-C WP，并希望调试我的ACSL注释(以理解为什么验证者说我“不知道”)。我有一些绿色或橙色的结果。我打开why3集成开发环境，看到生成的脚本。然后，我从列表中选择一个理论/目标，并能够启动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中“转到末尾”时，我看到一个错误“试图保存不完整的证明”。如何在Coq IDE中获得在frama-c或why3结果窗口中看到的“已证实”或“未知”结果？还有什么更好的方法来理解为什么我从证明者那里得到了“我不知道”的消息，并决定我的程序是否有bug或一段糟糕的ACSL规范？

Answer 1

Coq中的“尝试保存不完整的证明”在Frama-C/WP中被翻译为“未知”。事实上，Frama-C正在等待您以交互方式完成intros ...和Qed之间的证明。如果您成功地使Coq满意，保存脚本将允许您有一个绿色(或黄绿色)项目符号(“已证明”)。

关于你的第二个问题，尝试交互式地执行证明确实是理解问题所在的一个好方法。除了Coq之外，您还可以使用Why3已知的交互式验证器(如果我没记错的话，是Isabelle和PVS )，以及直接在WP，TIP中构建的新交互式验证器(请参阅the WP manual的第2.3节)。