Commit 32300303 authored by Simon Hudon's avatar Simon Hudon
Browse files

Add test case for Xchg

parent 1229cc72
......@@ -267,6 +267,37 @@ goal 2 is:
--------------------------------------∗
WP #() #() @ E ∖ ↑N {{ _, |={E ∖ ↑N}=> ▷ P ∗ True }}
"xchg_example"
: string
1 goal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
v₁, v₂ : val
Φ : val → iPropI Σ
============================
"Hl" : l ↦ v₂
"HΦ" : l ↦ v₂ -∗ Φ v₁
--------------------------------------∗
|={⊤}=> Φ v₁
1 goal
Σ : gFunctors
heapG0 : heapG Σ
N : namespace
l : loc
v : val
Φ : language.val heap_lang → iPropI Σ
v' : val
============================
"HΦ" : ∀ v'0 : language.val heap_lang, True -∗ Φ v'0
"Hl" : l ↦ v
"Hclose" : ▷ (∃ v0 : val, l ↦ v0) ={⊤ ∖ ↑N,⊤}=∗ emp
--------------------------------------∗
|={⊤ ∖ ↑N,⊤}=> Φ v'
1 goal
Σ : gFunctors
......
......@@ -333,7 +333,7 @@ Section mapsto_tests.
(* Loading from the general mapsto for any [dfrac]. *)
Lemma general_mapsto dq l v :
[[{ l {dq} v }]] ! #l [[{ RET v; True }]].
Proof.
Proof.
iIntros (Φ) "Hl HΦ". Show. wp_load. by iApply "HΦ".
Qed.
......@@ -382,6 +382,30 @@ Section atomic.
(* Test if a side-condition for [Atomic] is generated *)
iIntros (?) "H". iInv "H" as "H". Show.
Abort.
Check "xchg_example".
Lemma xchg_example l (v v : val) :
{{{ l v }}}
Xchg #l v
{{{ RET v; l v }}}.
Proof.
iIntros (Φ) "Hl HΦ".
wp_xchg.
Show.
Abort.
Lemma xchg_inv_example N l (v : val) :
{{{ inv N ( v, l v) }}}
Xchg #l v
{{{ v', RET v'; True }}}.
Proof.
iIntros (Φ) "Hl HΦ".
iInv "Hl" as (v') "Hl" "Hclose".
wp_xchg.
Show.
Abort.
End atomic.
Section printing_tests.
......
Supports Markdown
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