Coqインタラクティブ定理証明書でFrama-c WPプラグインを実行するには？

Question

スワップの例のフォーム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のは、それに残った3つのすべての証明義務のためUnknownを返します。

正常ですか？なぜ？

手動で証明書を手動で証明するはずですか？

誰でもこの例をcoqで正常に実行できますか？

バージョン; Frama-cマグネシウム-20151002、Coq8.4.6、MacOS1011.4で動作するOCaml4.02.3

Answer 1

実際、Coqは対話型定理証明者である。つまり、自分で証明書を書かなければならないということです（いくつかのデフォルトの戦術が試されるかもしれませんが、一般的に手作業で終わることになります）。 coq：frama-c -wp -wp-rte -wp-proof coqide swap.cの代わりにcoqideを使用して目標を確認できます。