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

Question

我使用 frama-C WP 并想调试我的 ACSL 注释（以了解为什么证明者说我“不知道”）。我有一些绿色或橙色的结果。我打开 why3 IDE 并查看生成的脚本。然后我从列表中选择一个理论/目标并能够启动 Alt-Ergo 或 Coq IDE。我想在 Coq IDE 中使用生成的代码。我看到一些公理，然后是 Theorem 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 中的“未知”翻译。事实上，Frama-C 正在等待你以交互方式完成 和 之间的intros ...证明Qed。如果你成功地让 Coq 开心，保存脚本会让你有一个绿色（或黄绿色）的子弹（“证明”）。

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