Commit 53d00192 authored by Léon Gondelman's avatar Léon Gondelman

tests: swap function

parent 70242f9c
......@@ -37,13 +37,46 @@ Section test.
Qed.
Definition swap_aform (l1 l2 : loc) : val := λ: <>,
(a_bind (λ: "r",
((a_bind (λ: "v", (a_store (a_ret "r")) (a_ret "v"))) (a_load (a_ret #l1))) ;;;
a_seq #();;;
((a_bind (λ: "v", (a_store (a_ret #l1)) (a_ret "v"))) (a_load (a_ret #l2))) ;;;
a_seq #();;;
((a_bind (λ: "v", (a_store (a_ret #l2)) (a_ret "v"))) (a_load (a_ret "r"))) ;;;
a_seq #()))
(a_alloc (a_ret #0)).
Lemma swap_spec_aform (l1 l2 : loc) (v1 v2: val) R :
l1 U v1 - l2 U v2 -
awp (swap_aform l1 l2 #()) R (λ _, l1 U v2 l2 U v1).
Proof.
iIntros "Hl1 Hl2".
(* let r = ref 0 in *)
awp_lam; iApply awp_bind; iApply (a_alloc_spec R #0); iIntros (r) "Hr".
(* r <- !l1 ; *)
awp_lam; do 2 iApply awp_bind; iApply (a_load_spec with "[$Hl1]"); iIntros "Hl1".
awp_lam; iApply (a_store_spec with "Hr"); iIntros "Hr"; awp_seq.
iApply awp_bind. iApply a_seq_spec; iUnlock.
(* l1 <- !l2 ; *)
awp_lam; do 2 iApply awp_bind; iApply (a_load_spec with "[$Hl2]"); iIntros "Hl2".
awp_lam; iApply (a_store_spec with "Hl1"); iIntros "Hl1"; awp_seq.
iApply awp_bind. iApply a_seq_spec. iUnlock.
(* l2 <- !r ; *)
awp_lam. do 2 iApply awp_bind. iApply (a_load_spec with "[$Hr]"); iIntros "Hr".
awp_lam; iApply (a_store_spec with "Hl2"); iIntros "Hl2"; awp_seq.
iApply a_seq_spec; iUnlock.
(* Post-condition*)
by iFrame.
Qed.
Definition swap (l1 l2 : loc) : val := λ: <>,
a_bind (λ: "r",
a_sequence
(a_store (a_ret "r") (a_load (a_ret #l1)))
(a_bind (λ: "v", (a_store (a_ret "r") (a_ret "v"))) (a_load (a_ret #l1)))
(a_sequence
(a_store (a_ret #l1) (a_load (a_ret #l2)))
(a_store (a_ret #l2) (a_load (a_ret "r")))))
(a_store (a_ret #l2) (a_load (a_ret "r")))) ;;; a_seq #() )
(a_alloc (a_ret #0%V)).
Lemma swap_spec (l1 l2 : loc) (v1 v2: val) R :
......@@ -55,7 +88,9 @@ Section test.
iApply awp_bind.
iApply (a_alloc_spec R #0 ).
iIntros (r) "Hr".
awp_lam.
Admitted.
awp_lam. iApply awp_bind.
Admitted.
End test.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment