0

2 つの関数の証明をプログラム全体の証明にまとめようとしています。

...
Definition Vprog : varspecs := nil.
Definition Gprog : funspecs := get_spec :: set_spec :: nil.

Lemma body_get: semax_body Vprog Gprog f_get get_spec.
Proof.
...
Qed.

Lemma body_set: semax_body Vprog Gprog f_set set_spec.
Proof.
...
Qed.

Existing Instance NullExtension.Espec.


Theorem all_funcs_correct:
  semax_func Vprog Gprog (prog_funct prog) Gprog.
Proof.
semax_func_skipn.
semax_func_cons body_get.

戦術を適用する前にsemax_func_cons、次の目標があります。

1 subgoals, subgoal 1 (ID 3951)

  ============================
   semax_func Vprog [get_spec; set_spec]
     [(_get, Internal f_get); (_set, Internal f_set)]
     [(_get,
      WITH x : share * Z * (Z -> val) * val * val PRE  [
      (_key, tint), (_rez, tint), (_arr, tptr tint)]
      (let (p, varr) := x in
       let (p0, vk) := p in
       let (p1, arr) := p0 in
       let (sh, k) := p1 in
       PROP  (0 <= k < 100; forall i : Z, 0 <= i < 100 -> is_int (arr i);
       repr k vk)
       LOCAL  (`(eq vk) (eval_id _key); `(eq varr) (eval_id _arr);
       `isptr (eval_id _arr))
       SEP  (`(array_at tint sh arr 0 100) (eval_id _arr))) POST  [tint]
      (let (p, varr) := x in
       let (p0, _) := p in
       let (p1, arr) := p0 in
       let (sh, k) := p1 in
       `(array_at tint sh arr 0 100 varr) && local (`(eq (arr k)) retval)));
     set_spec]

f_getしたがって、証明された lemma で消去するのが妥当と思われbody_getます。なぜ作戦は失敗するのか?

メッセージは役に立ちません：

Toplevel input, characters 0-24:
Error: No applicable tactic.
4

1 に答える 1

0

問題は引数リストの指定にあります。

  • 関数の引数のみが含まれている必要があります (ローカル変数は含まれません)。

  • C 関数プロトタイプと同じ順序で引数が必要です。

ところで、Gprog の関数の順序は、c ファイルの関数定義の順序と同じでなければなりません。

于 2015-01-15T10:54:32.867 に答える