spec.v 1.34 KB
Newer Older
1 2 3 4
From stdpp Require Import namespaces.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export proofmode notation.

5 6 7 8 9 10 11 12 13 14 15 16 17
(** General (HoCAP-style) spec for a concurrent bag ("per-elemt spec") *)
Record concurrent_bag {Σ} `{!heapG Σ} := ConcurrentBag {
  mk_bag : val;
  mk_bag_spec (N : namespace) (P : val  iProp Σ) :
    {{{ True }}}
      mk_bag #()
    {{{ (f f : val), RET (f, f);
        ( WP f #() {{ v, ( (v' : val), v  SOMEV v'  P v')    v  NONEV }})
         ( (v : val),  (P v - WP f v {{ v, True }}))
    }}}
}.
Arguments concurrent_bag _ {_}.

18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34
(** General (HoCAP-style) spec for a concurrent stack *)

Record concurrent_stack {Σ} `{!heapG Σ} := ConcurrentStack {
  mk_stack : val;
  mk_stack_spec (N : namespace) (P : list val  iProp Σ)
    (Q : val  iProp Σ) (Q' Q'' : iProp Σ) :
    {{{ P [] }}}
      mk_stack #()
    {{{ (f f : val), RET (f, f);
        ( ( ( v vs, P (v :: vs) ={   N}= Q v  P vs)
              (P [] ={   N}= Q'  P []) -
            WP f #() {{ v, ( (v' : val), v  SOMEV v'  Q v')  (v  NONEV  Q')}}))
         ( (v : val),
              (( vs, P vs ={   N}= P (v :: vs)  Q'') - WP f v {{ v, Q'' }}))
    }}}
}.
Arguments concurrent_stack _ {_}.