blob: d7a38e14e8ed3940bec18b1963558ec1e6f780f9 (
about) (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
|
From iris.program_logic Require Import atomic.
From iris.heap_lang Require Import notation proofmode.
From lmpmc Require Import util.
Record basic_queue {Σ} `{!heapGS Σ} :=
BasicQueue
{ new : val;
enqueue : val;
try_dequeue : val;
queue_repr : loc → list val → iProp Σ;
#[global] queue_repr_timeless ℓ vs :: Timeless (queue_repr ℓ vs);
new_spec :
{{{ True }}}
new #()
{{{ (ℓ_q : loc), RET #ℓ_q; queue_repr ℓ_q [] }}};
enqueue_spec (ℓ_q : loc) (data : val) :
⊢ <<{ ∀∀ vs, queue_repr ℓ_q vs }>>
enqueue #ℓ_q data @ ∅
<<{ queue_repr ℓ_q (vs ++ [data]) | RET #() }>>;
try_dequeue_spec (ℓ_q : loc) :
⊢ <<{ ∀∀ vs, queue_repr ℓ_q vs }>>
try_dequeue #ℓ_q @ ∅
<<{ queue_repr ℓ_q (tail vs) | RET (val_opt_hl (head vs)) }>>;
}.
#[global] Arguments basic_queue _ {_} : assert.
|
