1

更新：今、私は次のプログラムを持っていますswap.c：

void swap (int* a, int* b) {
  int ta = *a;             
  int tb = *b;            
  ta = ta ^ tb;
  tb = ta ^ tb;
  ta = ta ^ tb;
  *a = ta;
  *b = tb;                           
}

私の仕様は

Require Import floyd.proofauto.
Require Import floyd.entailer.
Require Import veric.SeparationLogic.

Require Import swap.

Local Open Scope logic.
Local Open Scope Z.

Definition swap_spec :=
  DECLARE _swap
   WITH sh : share, aptr : val, a : int, bptr : val, b : int
     PRE [ _a OF (tptr tint), _b OF (tptr tint)]
       PROP ()
       LOCAL (`(eq aptr) (eval_id _a);
              `(eq bptr) (eval_id _b))
       SEP (` (mapsto sh tint aptr (Vint a));
            ` (mapsto sh tint bptr (Vint b)))
       POST [tint] (`(mapsto sh tint aptr (Vint b)) *
                    `(mapsto sh tint bptr (Vint a))).

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

Lemma body_swap : semax_body Vprog Gprog f_swap swap_spec.
Proof.
  start_function.
  forward.
  forward.
  forward.
  forward.
  forward.  
  eapply semax_seq.
  eapply semax_seq.

今、私は立ち往生しています:私は展開することができ、展開eval_binopを進めようとしますが、実際には作業できるものに収束しません。さらに、`eq プロパティを使用して実際に何かを書き換える方法もわかりません。

4

1 に答える 1

1

あなたの仕様は正しいようです。

Verifiable C の標準的な分離ロジックでは、C ステートメントごとに 1 つのロードまたはストアしか推論できないため、コードを次のように書き直す必要があります。

ta = *a; tb = *b; *a = ta^tb;
ta = *a; tb = *b; *b = ta^tb;
ta = *a; tb = *b; *a = ta^tb;
于 2015-08-10T12:40:52.963 に答える