0

今回は他を呼び出す関数を証明しています。vars.c:

int pure0 ()
{
    return 0;
}

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

私の証明開始 - verif_vars.v:

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).

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.
  forward_call (sh).
  entailer!.

目標を誘導するもの：

2 subgoals, subgoal 1 (ID 566)

  Espec : OracleKind
  sh : share
  arr : Z -> val
  varr : val
  Delta := abbreviate : tycontext
  POSTCONDITION := abbreviate : ret_assert
  MORE_COMMANDS := abbreviate : statement
  Struct_env := abbreviate : type_id_env.type_id_env
  arrarg : name _arr
  ============================
   Forall (closed_wrt_vars (eq _z')) [`(array_at tint sh arr 0 100 varr)]

subgoal 2 (ID 567) is:
 DO_THE_after_call_TACTIC_NOW

関数呼び出しは内容を変更しないと述べていると思いますがarr、これは私にとっては明らかです。

この目標に対して何ができるでしょうか？ここで適用される戦術はどれですか?また、このステートメントは正確には何を意味していますか? 仕様を充実させpure0て、何も変更しないことを何らかの形で指摘する必要がありますか?

4

3 に答える 3

1

最初に: VST/Verifiable-C に関する質問を書くときは、使用している VST のバージョンを示してください。1.4を使用しているようです。

2番目: これですべての質問に答えられるかどうかはわかりませんが、

"closed_wrt_vars S P" は、リフトされたアサーション P がセット S 内のすべての変数に関して閉じていることを示します。つまり、S は、アドレス指定できないローカル変数 ("vars 」）。P は "environ->mpred" という形式の表明であり、"closed" は、"environ" を変更して集合 S の変数のいずれかに対して異なる値を持たせた場合、P の真は変化しないことを意味します。

「Forall」は、述語をリストに適用するための Coq の標準ライブラリ述語です。そう、

 Forall (closed_wrt_vars (eq _z')) [`(array_at tint sh arr 0 100 varr)]

つまり、セット S を変数 _z' だけを含むシングルトン セットとします。ここで、リスト内のすべての述語は S に関して閉じていると断言します。リスト内の述語は 1 つだけであり、それは「自明に持ち上げられた」ものです。つまり、どの述語 (P: mpred) についても、持ち上げられた述語です。

`(P)

(fun rho:environ => P) と同等です。したがって、自明なことに、`P は、_z の値を変更することを含め、rho に対して何をしてもかまいません'。

「auto with closed」(または念のために言うと、「auto 50 with closed」) がこれを処理する必要があり、それを処理することを示します。それで、あなたの質問の残りは「ここで何が起こっているのですか?」だったと思います。

于 2015-01-18T17:27:16.177 に答える
0

で使用されるソリューションvst/progs/verif_reverse.v:

auto with closed.

残念ながら、それは質問の半分しか答えません。

于 2015-01-18T15:05:32.313 に答える