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

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 中“走到最后”时，我看到错误“尝试保存不完整的证明”。如何在 Coq IDE 中获得在 frama-c 或 Why3 结果窗口中看到的“已证明”或“未知”结果？ 有什么更好的方法来理解为什么我从证明者那里收到“我不知道”的消息，并确定我的程序是否存在错误或不良的 ACSL 规范？

Answer 1

Coq 中的“尝试保存不完整的证明”在 Frama-C/WP 中被翻译为“Unknown”。事实上，Frama-C 正在等待您交互地完成 intros ... 和 Qed 之间的证明。如果你成功地让 Coq 高兴，保存脚本将让你得到一个绿色(或黄绿色)的子弹(“已证明”)。

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