这是交换示例表单WP插件教程；
/*@ requires \valid(a) && \valid(b);
@ ensures A: *a == \old(*b) ;
@ ensures B: *b == \old(*a) ;
@ assigns *a,*b ;
@*/
void swap(int *a, int *b)
{
int tmp;
tmp = *a;
*a = *b;
*b = tmp;
return;
}
这是当我用coq在其上运行frama-c时的结果；
frama-c -wp -wp-rte -wp-proof coq swap.c
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing swap.c (with preprocessing)
[rte] annotating function swap
[wp] 9 goals scheduled
[wp] [Coq] Goal typed_swap_assert_rte_mem_access : Unknown
[wp] [Coq] Goal typed_swap_post_A : Unknown
[wp] [Coq] Goal typed_swap_assert_rte_mem_access_3 : Unknown
[wp] Proved goals: 6 / 9
Qed: 6 (0.13ms-0.71ms-2ms)
Coq: 0 (unknown: 3)
因此，Coq会退还Unknown所有剩余的三个证明义务。
正常吗 为什么呢？
我是否应该每年为他们手动证明证据？
任何人都可以让这个示例与Coq一起运行吗？
版本；在MacOS 10.11.4上运行的Frama-c Magnesium-20151002，Coq 8.4.6，OCaml 4.02.3
确实，Coq是交互式定理证明者。这意味着您必须自己编写证明（也许尝试了一些默认策略，但通常最终还是要手动完成）。您可以看到使用的目标coqide，而不是coq：frama-c -wp -wp-rte -wp-proof coqide swap.c。
本文收集自互联网，转载请注明来源。
如有侵权，请联系[email protected] 删除。
我来说两句