如何用Coq交互式证明器完成Frama-C WP未证的4项证明义务？

第一步：导出未证的Coq证明目标 #

先把WP生成的未证证明义务导出为Coq格式文件，替代过时的GUI操作：

frama-c -wp -wp-coq -wp-out ./coq_proofs bubble_sort.c

• -wp-coq：指定WP生成Coq格式的证明义务
• -wp-out ./coq_proofs：将所有Coq相关文件输出到coq_proofs目录，方便管理

导出完成后进入该目录，找到文件名包含_obligation_和对应编号的.v文件（编号对应WP输出中超时未证的义务序号）。

第二步：定位目标证明义务 #

先从frama-c -wp bubble_sort.c的输出里，记录超时未证的义务编号（比如输出里的[wp] Warning: Proof obligation ... timed out信息），然后在coq_proofs目录里找到对应编号的.v文件。

第三步：用Coq工具链交互式完成证明 #

因为无法使用frama-c-gui，直接用标准Coq工具处理导出的文件：

1. 确保Mac ARM64环境已安装Coq，可通过Homebrew安装：brew install coq
2. 用CoqIDE打开目标.v文件，或者用VsCode配合VsCoq插件操作
3. 逐行执行Coq脚本，在WP自动证明超时的步骤处，手动补充证明策略

针对排序类证明的常用技巧 #

这类义务通常涉及数组排列、循环不变量或终止性，常用策略：

• 用induction处理数组索引的归纳性质
• 用rewrite展开WP生成的Permut（排列）、Sorted（有序）等谓词定义
• 用assert引入中间引理，拆分复杂证明逻辑
• 用auto/intuition自动处理简单逻辑推导

比如处理数组交换后的排列性质时，可手动添加：

assert (Permut (a[i] :: a[j] :: rest) (a[j] :: a[i] :: rest)); auto.

第四步：导入已完成的证明并验证 #

完成手动证明后保存.v文件，回到Frama-C执行以下命令，让WP加载并验证你的手动证明：

frama-c -wp -wp-coq-load ./coq_proofs bubble_sort.c

前置优化：减少手动证明的工作量 #

如果不想直接手动证明，可先尝试调整WP参数，提升自动证明成功率：

• 延长超时时间：frama-c -wp -wp-timeout 60 bubble_sort.c（将超时设为60秒，默认通常为10秒）
• 启用多 prover 并行尝试：frama-c -wp -wp-prover alt-ergo,z3 bubble_sort.c（需提前安装对应 prover）

内容的提问来源于stack exchange，提问作者Meir Benayoun