enrich
   map, 
   polyref
with
   procedures alloc#  : Map[Ref[A], A] → Ref[A] nonfunctional nondeterministic;
   variables 
       h : Map[Ref[A], A];
       r : Ref[A];
       a : A;
       n : Nat;
       hP : Map[Ref[A], A] → Bool;
       b : B;
       c : C;
       d : D;
   
   partial functions 
       . +h . : Map[Ref[A], A] × Ref[A] → Map[Ref[A], A] prio 9 left with λ h, r. ¬ null ∈ h ∧ r ≠ null ∧ ¬ r ∈ h;
       . [ . ]h : Map[Ref[A], A] × Ref[A] → A with λ h, r. ¬ null ∈ h ∧ r ≠ null ∧ r ∈ h;
       . [ . := . ]h : Map[Ref[A], A] × Ref[A] × A → Map[Ref[A], A] with λ h, r, o. ¬ null ∈ h ∧ r ≠ null ∧ r ∈ h;
       . --h . : Map[Ref[A], A] × Ref[A] → Map[Ref[A], A] prio 9 left with λ h, r. ¬ null ∈ h ∧ r ≠ null ∧ r ∈ h;
   
   
   axioms 
      get-def: h[r]h = h(r);
      used for: s, ls;
      
      put-def: r ∈ h → h[r := a]h = h(r := a);
      used for: s, ls;
      
      put-undef: ¬ r ∈ h → h[r := a]h = h;
      used for: s, ls;
      
      del-def: h --h r = h -- r;
      used for: s, ls;
      
      add-size: ¬ r ∈ h, r ≠ null ⊦ #(h +h r) = # h + 1;
      used for: s, ls;
      
      add-get: ¬ r ∈ h, r ≠ null ⊦ r0 ≠ r → (h +h r)(r0) = h(r0);
      used for: s, ls;
      
      add-in: ¬ r ∈ h, r ≠ null ⊦ r0 ∈ h +h r ↔ r0 ∈ h ∨ r0 = r;
      used for: s, ls;
   
   declarations 
      alloc: 
      alloc#(; h){choose r0 with ¬ r0 ∈ h ∧ r0 ≠ null in {h := h +h r0; r0} ifnone null};
      
      
   
   
end enrich