generic specification
   
parameter
   refobj

   using nat, refset
target
   sorts heap;
   constants  ∅ : heap;
   functions  . ++ . : heap × ref → heap prio 9 left;
              . -- . : heap × ref → heap prio 9 left;
              . [ . ] : heap × ref → obj;
              . [ . ] : heap × ref × obj → heap;
              # . : heap → nat;
              . ∪ . : heap × heap → heap;
              . \ . : heap × refset → heap;
              . \ . : heap × heap → heap;
              dom . : heap → refset;
   predicates  . ∈ . : ref × heap;
               . ⊆ . : heap × heap;
               . ⊥ . : heap × heap;
   variables  h : heap;
              rs : refset;
              r : ref;
              o : obj;
              d : obj;
              hP : heap → bool;
   induction heap generated by ∅, ++, [ ];

   axioms 
      ext :  ⊦ h0 = h1 ↔ (∀ r. (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r]));
      dom :  ⊦ r ∈ dom h ↔ r ∈ h;
      used for: s, ls;
      subset :  ⊦ h0 ⊆ h1 ↔ (∀ r. (r ∈ h0 → r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r]));
      sanity :  ⊦ ¬ null ∈ h;
      used for: s, ls;
      in-emp :  ⊦ ¬ r ∈ ∅;
      used for: s, ls;
      in-alloc : r0 ≠ null, ¬ r0 ∈ h ⊦ r ∈ h ++ r0 ↔ r = r0 ∨ r ∈ h;
      used for: s, ls;
      in-write :  ⊦ r ∈ h[r0, o] ↔ r ∈ h;
      used for: s, ls;
      at-alloc : r ∈ h, r0 ≠ null, ¬ r0 ∈ h ⊦ r ≠ r0 → (h ++ r0)[r] = h[r];
      used for: s, ls, c, lc;
      at-write :  ⊦ h[r0, o][r] = (r = r0 ∧ r0 ∈ h ⊃ o;h[r]);
      used for: s, ls;
      in-del :  ⊦ r ∈ h -- r0 ↔ r ≠ r0 ∧ r ∈ h;
      used for: s, ls;
      at-del : r ∈ h ⊦ r ≠ r0 → (h -- r0)[r] = h[r];
      used for: s, ls;
      uni-emp :  ⊦ h0 ∪ ∅ = h0;
      used for: s, ls;
      uni-alloc : r ≠ null, ¬ r ∈ h1, ¬ r ∈ h0, h0 ⊥ h1 ⊦ h0 ∪ (h1 ++ r) = (h0 ∪ h1) ++ r;
      used for: s, ls;
      uni-write : r ≠ null, r ∈ h1, h0 ⊥ h1 ⊦ h0 ∪ h1[r, o] = (h0 ∪ h1)[r, o];
      used for: ls;
      diff-emp :  ⊦ h0 \ ∅ = h0;
      used for: s, ls;
      diff-alloc : r ≠ null, ¬ r ∈ h1 ⊦ h0 \ (h1 ++ r) = (h0 -- r) \ h1;
      used for: s, ls;
      diff-write : r ∈ h1 ⊦ h0 \ h1[r, o] = h0 \ h1;
      used for: s, ls;
      diffs-emp :  ⊦ h0 \ ∅ = h0;
      used for: s, ls;
      diffs-ins :  ⊦ h0 \ (rs ++ r) = (h0 -- r) \ rs;
      used for: s, ls;
      disj :  ⊦ h0 ⊥ h1 ↔ (∀ r. ¬ r ∈ h0 ∨ ¬ r ∈ h1);
      size-emp :  ⊦ # ∅ = 0;
      used for: s, ls;
      size-alloc : ¬ r ∈ h, r ≠ null ⊦ #(h ++ r) = # h + 1;
      used for: s, ls;
      size-write : r ∈ h ⊦ # h[r, o] = # h;
      used for: s, ls;

   
end generic specification