0

私の簡単なプログラムはvars.c次のとおりです。

int pure0 ()
{
    return 0;
}

int get0(int* arr)
{
    int z = pure0();
    return z;
}

証明を開始しました (ファイルverif_vars.c):

Require Import floyd.proofauto.
Require Import vars.

Local Open Scope logic.
Local Open Scope Z.

Definition get0_spec :=
  DECLARE _get0
    WITH sh : share, arr : Z->val, varr : val
    PRE [_arr OF (tptr tint)]
        PROP ()
        LOCAL (`(eq varr) (eval_id _arr);
               `isptr (eval_id _arr))
        SEP (`(array_at tint sh arr 0 100) (eval_id _arr))
    POST [tint] `(array_at tint sh arr 0 100 varr) &&
                 local(`(eq (Vint (Int.repr 0))) retval).

Definition pure0_spec :=
  DECLARE _pure0
    WITH sh : share
    PRE []
        PROP ()
        LOCAL ()
        SEP ()
    POST [tint] local(`(eq (Vint (Int.repr 0))) retval).

Definition Vprog : varspecs := nil.
Definition Gprog : funspecs := get0_spec :: pure0_spec ::nil.

Lemma body_pure0: semax_body Vprog Gprog f_pure0 pure0_spec.
Proof.
  start_function.
  forward.
Qed.


Lemma body_get0: semax_body Vprog Gprog f_get0 get0_spec.
Proof.
  start_function.
  name arrarg _arr.
  name zloc _z.
  name zloc' _z'.
  forward_call (sh).
  entailer!.
  auto with closed.
  after_call.
  forward.
  entailer!.

最終的に 2 つのサブゴールができました。

  Espec : OracleKind
  sh : share
  arr : Z -> val
  Struct_env := abbreviate : type_id_env.type_id_env
  Delta := abbreviate : tycontext
  zloc0 : val
  arrarg : val
  zloc : int
  TC : is_pointer_or_null arrarg
  Parrarg : isptr arrarg
  ============================
   Int.repr 0 = zloc

subgoal 2 (ID 1273) is:
 !!(Int.repr 0 = zloc) |-- emp
  • 最初のものはpure0_spec事後条件から直接続きます。しかし、どうすればそれをCoqに伝えることができますか?
  • admit. entailer.2 番目の目標は ( によって) に簡略化できますTT |-- emp。これも些細なことのように思えますが、それでもどうやってそれを証明できますか (SearchAbout derivesそしてSearchAbout emp一般的な補題を示していません)?

私が使用するもの: VST 1.5 (2014-10-02 で 6834P)、CompCert 2.4、Coq 8.4pl3(Jan'14) with OCaml 4.01.0。

4

1 に答える 1

1

最初に、これを自分で再現しようとせずに、（文書化されているように）証明可能な目標を証明できない目標に変えることがあるentailer!ため、使用が「危険」すぎる可能性があります。entailer!前髪なしで試してみてentailer、見栄えが良くなるかどうかを確認してください。

第二に、 そうでTT |-- empはありません。 TT任意のヒープにemp適用され、空のヒープにのみ適用されます。pure関数の事後条件を次のように変更することで、これを修正できます。

POST [tint] local(`(eq (Vint (Int.repr 0))) retval) && emp.
于 2015-01-18T19:13:06.660 に答える