0

今、簡単な配列アクセス手順 (ファイル arr.c) を証明しようとしています:

void set(int* arr, int key, int val)
{
    arr[key] = val;
}

ファイルarr.cは次のように変換されarr.vます:

...
Definition f_set := {|
  fn_return := tvoid;
  fn_callconv := cc_default;
  fn_params := ((_arr, (tptr tint)) :: (_key, tint) :: (_val, tint) :: nil);
  fn_vars := nil;
  fn_temps := nil;
  fn_body :=
(Sassign
  (Ederef
    (Ebinop Oadd (Etempvar _arr (tptr tint)) (Etempvar _key tint)
      (tptr tint)) tint) (Etempvar _val tint))
|}.
...

これが私の証明の始まりです (ファイル verif_arr.v):

Require Import floyd.proofauto.
Require Import arr.

Local Open Scope logic.
Local Open Scope Z.

Inductive repr : Z -> val -> Prop :=
| mk_repr : forall z, z >= 0 -> z < Int.modulus -> repr z (Vint (Int.repr z)).

Function aPut (arr:Z -> val) (k:Z) (v:val) : Z -> val :=
  fun (kk:Z) => if (Z.eq_dec k kk) then v else arr kk.

Definition set_spec :=
  DECLARE _set
    WITH sh : share, k : Z, arr : Z->val, vk : val, v : val, varr : val
    PRE [_key OF tint, _val OF tint, _arr OF (tptr tint)]
        PROP (0 <= k < 100; forall i, 0 <= i < 100 -> is_int (arr i);
              writable_share sh; repr k vk)
        LOCAL (`(eq vk) (eval_id _key);
               `(eq varr) (eval_id _arr);
               `(eq v) (eval_id _val);
               `isptr (eval_id _arr))
        SEP (`(array_at tint sh arr
                        0 100) (eval_id _arr))
    POST [tvoid] `(array_at tint sh (aPut arr k v)
                            0 100 varr).

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

Lemma body_set: semax_body Vprog Gprog f_set set_spec.
Proof.
  start_function.
  name karg _key.
  name arrarg _arr.
  name valarg _val.
  forward.
  entailer!.

戦術の後entailer!.、私は持っています：

3 subgoals, subgoal 1 (ID 1261)

  Espec : OracleKind
  sh : share
  k : Z
  arr : Z -> val
  H : 0 <= k < 100
  H0 : forall i : Z, 0 <= i < 100 -> is_int (arr i)
  H1 : writable_share sh
  Delta := abbreviate : tycontext
  MORE_COMMANDS := abbreviate : statement
  Struct_env := abbreviate : type_id_env.type_id_env
  karg : name _key
  arrarg : name _arr
  valarg : name _val
  rho : environ
  H2 : repr k (eval_id _key rho)
  POSTCONDITION := abbreviate : ret_assert
  H3 : isptr (eval_id _arr rho)
  ============================
   offset_val (Int.repr (sizeof tint * 0)) (eval_id _arr rho) =
   force_val (sem_add_pi tint (eval_id _arr rho) (eval_id _key rho))

subgoal 2 (ID 1266) is:
 ?890 = force_val (sem_cast_neutral (eval_id _val rho))
subgoal 3 (ID 1235) is:
 semax Delta
   (PROP  ()
    LOCAL  (`(eq vk) (eval_id _key); `(eq varr) (eval_id _arr);
    `(eq v) (eval_id _val); `isptr (eval_id _arr))
    SEP  (`(array_at tint sh (upd arr 0 ?890) 0 100) (eval_id _arr)))
   (Sreturn None) POSTCONDITION

今質問：

  • 仕様set_specには前提条件があり'(array_at tint sh arr 0 100) (eval_id _arr)ます (ここで'は、フォーマットを壊すバッククォートにする必要はありません)。このステートメントが仮説リストにないのはなぜですか?

  • 最初のサブゴールは、配列の 0 セル (arr + 0) を逆参照しようとしているように思えます。これは、キー番目のセル (arr + key) と等しくなければなりません。それはコードや事後条件とは何の関係もなく、確かに証明できません。ここで何がうまくいかなかったのですか？

私が使う：

VST バージョン:

Definition svn_rev := "6834P".
Definition release := "1.5".
Definition date := "2014-10-02".

CompCert バージョン: 2.4

コックのバージョン:

The Coq Proof Assistant, version 8.4pl3 (January 2014)
compiled on Jan 19 2014 23:14:16 with OCaml 4.01.0

編集：

投稿条件の最後のlocal ...部分は冗長であることが判明しました。

4

1 に答える 1

0

  • まず、前提条件はデルタ仮説'(array_at tint sh arr 0 100) (eval_id _arr)の背後に実際に存在します。abbreviate

  • entailer!.第二に、その戦術は安全ではなく、適格な目標から証明できない目標を生み出す可能性があることが判明しました。この場合、

    • is_int vまず、「すべての整数」配列のセルに割り当てることができるように、追加の条件を指定する必要があります。どうやら VST は CompCert 注釈から型を推測できません。
    • そうすれentailer!.ば、最初に右辺のすべての命題を個別に証明する必要がなくなり、entailer仮説を組み合わせることができます。

正しい仕様と証拠は次のとおりです。

Inductive repr : Z -> val -> Prop :=
| mk_repr : forall z, z >= 0 -> z < Int.modulus -> repr z (Vint (Int.repr z)).

Function aPut (arr:Z -> val) (k:Z) (v:val) : Z -> val :=
  fun (kk:Z) => if (Z.eq_dec k kk) then v else arr kk.

Definition set_spec :=
  DECLARE _set
    WITH sh : share, k : Z, arr : Z->val, vk : val, v : val, varr : val
    PRE [_key OF tint, _val OF tint, _arr OF (tptr tint)]
        PROP (0 <= k < 100; forall i, 0 <= i < 100 -> is_int (arr i);
              writable_share sh; repr k vk; is_int v)
        LOCAL (`(eq vk) (eval_id _key);
               `(eq varr) (eval_id _arr);
               `(eq v) (eval_id _val);
               `isptr (eval_id _arr))
        SEP (`(array_at tint sh arr
                        0 100) (eval_id _arr))
    POST [tvoid] `(array_at tint sh (aPut arr k v)
                            0 100 varr).

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

Lemma body_set: semax_body Vprog Gprog f_set set_spec.
Proof.
  start_function.
  name karg _key.
  name arrarg _arr.
  name valarg _val.
  forward.
  instantiate (1:=v).
  instantiate (2:=k).
  assert (offset_val (Int.repr (sizeof tint * k)) (eval_id _arr rho) =
          force_val (sem_add_pi tint (eval_id _arr rho) (eval_id _key rho))).
  inversion H2.
  rewrite sem_add_pi_ptr.
  unfold force_val.
  apply f_equal2.
  rewrite mul_repr.
  auto.
  auto.
  assumption.

  assert (eval_id _val rho = force_val (sem_cast_neutral (eval_id _val rho))).
  apply is_int_e in H3.
  destruct H3 as [n VtoN].
  rewrite VtoN.
  auto.
  entailer.
  forward.
Qed.
于 2015-01-14T21:23:01.970 に答える