0

我正在尝试将我的两个功能的证明组合成整个程序的证明：

...
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用我证明的引理来消除似乎是合理的body_get。为什么战术失败？

该消息无济于事：

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

1 回答 1

0

问题出在参数列表规范中。

  • 它必须只包含函数参数（没有局部变量）

  • 它必须具有与 C 函数原型中相同顺序的参数。

顺便说一句，Gprog 中的函数顺序必须与 c 文件中函数定义的顺序相同。

于 2015-01-15T10:54:32.867 回答