enrich
   separation
with
   procedures alloc  : ref × heap nonfunctional nondeterministic;
              alloc# refset : ref × heap nonfunctional nondeterministic;
              read ref × heap :  : obj  ;
              write ref × obj : heap nonfunctional ;
              free ref : heap nonfunctional ;
   variables  h : heap;
              r : ref;
              o : obj;
              rs : refset;
   axioms 
      infinite-mem :  ⊦ ∃ r. ¬ r ∈ h ∧ r ≠ null;
      infinite-refs :  ⊦ ∃ r. ¬ r ∈ rs ∧ r ≠ null;

   declarations 
      alloc-decl : alloc(; r, h){choose r0 with ¬ r0 ∈ h ∧ r0 ≠ null in r := r0, h := h ++ r0};;
      
      alloc-refset-decl : alloc#(rs; r, h){choose r0 with ¬ r0 ∈ rs ∧ r0 ≠ null in r := r0, h := h ++ r0};;
      
      read-decl : read(r, h; o){if ¬ r ∈ h then abort else o := h[r]};;
      
      write-decl : write(r, o; h){if ¬ r ∈ h then abort else h[r] := o};;
      
      free-decl : free(r; h){if ¬ r ∈ h then abort else h := h -- r};;

   
end enrich