enrich storefuns with
   functions 
      init : classname × store → store;
       . ∪ . : store × store → store;
      comment: right entries supersede left entries.;
       
       . .refs : store → referenceset;
   predicates 
      exception : classname × store;
      classof : reference × classname × store;
      typeof : reference × javatype × store;
      has_type : reference × store;
      reftypep : javavalue × store;
       . =mode . : store × store;
      eqexmode : store × store × reference;
      eqex : store × store × reference;
      eqkeys : store × store;
      comment: two stores have the same keys;
       
      eqobjid : reference × store × store;
      comment: true if an object has the same fields in two stores.;
       
      eqobj : reference × store × store;
      comment: true if an object has the same fields and values in two stores.;
       
      onlyModified : reference × store × store;
      comment: true if only values of the given reference are modified
                              (the keys are unchanged and _type/_length values);
       
      onlyModified : references × store × store;
      comment: true if only values of the given references are modified
                              (the keys are unchanged and _type/_length values);
       
      uninit : classnameset × store;
      nouninit : classnameset × store;
      init : classnameset × store;
      comment: all classes in claset are 'initdone'.;
       
      initdone : classnames × store;
      comment: all classes are 'initdone'.;
       
      noiniterror : classnameset × store;
      initerror : classnameset × store;
   
   axioms 
      lookup-xtra :  ⊦ ∅[rk] = noval;
      used for : s, ls;
       
      union-empty :  ⊦ st ∪ ∅ = st;
      used for : s, ls;
       
      union-rec :  ⊦ st ∪ st0[rk, val] = (st ∪ st0)[rk, val];
      used for : ls;
       
      refs-def :  ⊦ r ∈ st .refs ↔ r ∈ st;
      initdone-def :  ⊦ initdone(classes, st) ↔ (∀ class. class ∈ classes → initdone(class, st));
      init :  ⊦ init(claset, st) ↔ (∀ class. class ∈ claset → initdone(class, st));
      uninit :  ⊦ uninit(claset, st) ↔ (∀ class. class ∈ claset → initundone(class, st));
      nouninit :  ⊦ nouninit(claset, st) ↔ (∀ class. class ∈ claset → ¬ initundone(class, st));
      initerror :  ⊦ initerror(claset, st) ↔ (∀ class. class ∈ claset → initerror(class, st));
      noiniterror :  ⊦ noiniterror(claset, st) ↔ (∀ class. class ∈ claset → ¬ initerror(class, st));
      init-def :  ⊦ init(class1, st) = st[jvmref -- mkfs(class1, void_type, `initstate' .field) ', initval(done)];
      eqkeys :  ⊦ eqkeys(st, st0) ↔ (∀ rk. rk ∈ st ↔ rk ∈ st0);
      reftypep :  ⊦ reftypep(val, st) ↔ is_referencevalue(val) ∧ (val .refval = jvmref ∨ val .refval ∈ st);
      classOf :  ⊦ classof(r, class1, st) ↔ r ≠ jvmref ∧ r -- _type ∈ st ∧ st[r -- _type] = typeval(mkclasstype(class1));
      typeOf :  ⊦ typeof(r, ty, st) ↔ r ≠ jvmref ∧ r -- _type ∈ st ∧ st[r -- _type] = typeval(ty);
      has_type :  ⊦ has_type(r, st) ↔ r ≠ jvmref ∧ r -- _type ∈ st ∧ is_typevalue(st[r -- _type]);
      exception :  ⊦ exception(class1, st) ↔ is_throw_mode(st[_mode]) ∧ st[_mode] .type = mkclasstype(class1);
      used for : ls;
       
      equalXmode
      : ⊦ 
          st =mode st0
        ↔ st = st0 ∨ (∃ r, class1. st = (st0[r -- _type, typeval(mkclasstype(class1))][_mode, throw(r, mkclasstype(class1))]) ∧ newref(r, st0));
      eqobjid
      : ⊦ 
          eqobjid(r, st, st0)
        ↔   (∀ sk. r -- sk ∈ st ↔ r -- sk ∈ st0) ∧ (r -- _type ∈ st → st[r -- _type] = st0[r -- _type])
          ∧ (r -- _length ∈ st → st[r -- _length] = st0[r -- _length]);
      eqobj :  ⊦ eqobj(r, st, st0) ↔ (∀ sk. (r -- sk ∈ st ↔ r -- sk ∈ st0) ∧ st[r -- sk] = st0[r -- sk]);
      eqexmode :  ⊦ eqexmode(st, st0, r) ↔ st -- r =mode st0 -- r;
      eqex :  ⊦ eqex(st, st0, r) ↔ st -- r = st0 -- r;
      onlyModifiedSet-def :  ⊦ onlyModified(refs, st1, st2) ↔ (∀ r. r ∈ refs → onlyModified(r, st1, st2));
      onlyModified
      : ⊦ 
          onlyModified(r, st1, st2)
        ↔   (∀ rk. rk ∈ st1 ↔ rk ∈ st2) ∧ (∀ r0, sk. r0 ≠ r → st1[r0 -- sk] = st2[r0 -- sk]) ∧ (r -- _type ∈ st1 → st1[r -- _type] = st2[r -- _type])
          ∧ (r -- _length ∈ st1 → st1[r -- _length] = st2[r -- _length]);
end enrich