Доказательство правильности Xor-Swapping

Question

Обновление: теперь у меня есть следующая программа 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, чтобы переписать что-либо.

Answer 1

Ваша спецификация выглядит правильно.

В стандартной разделительной логике Verifiable C вы можете рассуждать только об одной загрузке или сохранении для каждого оператора C, поэтому вам придется переписать код следующим образом:

ta = *a; tb = *b; *a = ta^tb;
ta = *a; tb = *b; *b = ta^tb;
ta = *a; tb = *b; *a = ta^tb;