enrich javastore , 
       refkeykeys , 
       refkeyvalues with
   functions 
      . [ . ] : store × storekey → javavalue;
      . [ . ] : store × storekeys → javavalue;
      . [ . ] : store × refkeykeys → javavalue;
      . [ . ] : store × storekey × javavalue → store;
      . [ . ] : store × storekeys × javavalue → store;
      . [ . ] : store × refkeykeys × javavalue → store;
      . [ . ] : store × refkeyvalues → store;
       . -- . : store × reference → store prio 9 left;
      _out : store → javavalue;
      newref : store → reference;
      maxref : store → reference;
      newref_list : nat × store → references;
      getrefs : reference × storekeys × store → references;
      comment: collect list of all visited references for the storekeys. 
                                Includes the top reference.;
       
      catch_break : store → store;
      catch_continue : store → store;
   predicates 
       . ∈ . : reference × store;
       . ∈ . : refkeykeys × store;
      normalmode : store;
      jump : store;
      newref : reference × store;
      is_a_newref : reference × store;
      is_the_newref : reference × store;
      is_newref_list : references × store;
      initerror : classname × store;
      initdone : classname × store;
      initundone : classname × store;
      init : store;
      comment: all (even non-existent) classes initialized.;
       
      init : string × store;
      comment: all existing classes initialized.;
       
      uninit : store;
      comment: all (including non-existent) classes undone.;
       
      uninit : string × store;
      comment: all existing classes undone.;
       
      initdoneP : classname × store;
      initundoneP : classname × store;
   variables 
      i1, i2 : int; 
   
   axioms 
      lookup-staticfield :  ⊦ st[sk] = st[jvmref -- sk];
      lookup-storerefs :  ⊦ st[sks] = st[jvmref -- sks];
      lookup-empty :  ⊦ st[r -- []] = refval(r);
      used for : s, ls;
       
      lookup-one :  ⊦ st[r -- sk '] = st[r -- sk];
      used for : s, ls;
       
      lookup-rec :  ⊦ st[r -- (sk ' + sk0 ' + sks)] = st[st[r -- sk] .refval -- (sk0 ' + sks)];
      put-staticfield :  ⊦ st[sk, val] = st[jvmref -- sk, val];
      put-storerefs :  ⊦ st[sks, val] = st[jvmref -- sks, val];
      put-one :  ⊦ st[r -- sk ', val] = st[r -- sk, val];
      used for : s, ls;
       
      put-rec :  ⊦ st[r -- (sk ' + sk0 ' + sks), val] = st[st[r -- sk] .refval -- (sk0 ' + sks), val];
      put-refkeyvalues-empty :  ⊦ st[[]] = st;
      used for : s, ls;
       
      put-refkeyvalues-rec :  ⊦ st[(rk × val) ' + rkvs] = (st[rk, val][rkvs]);
      used for : ls;
       
      getrefs-empty :  ⊦ getrefs(r, [], st) = r ';
      used for : s, ls;
       
      getrefs-rec :  ⊦ getrefs(r, sk ' + sks, st) = r ' + getrefs(st[r -- sk] .refval, sks, st);
      instore :  ⊦ r ∈ st ↔ (∃ sk. r -- sk ∈ st);
      instore-empty :  ⊦ r -- [] ∈ st ↔ r ∈ st;
      used for : s, ls;
       
      instore-one :  ⊦ r -- sk ' ∈ st ↔ r -- sk ∈ st;
      used for : s, ls;
       
      instore-rec :  ⊦ r -- (sk ' + sk0 ' + sks) ∈ st ↔ r -- sk ∈ st ∧ st[r -- sk] .refval -- (sk0 ' + sks) ∈ st;
      newref :  ⊦ newref(r, st) ↔ r ≠ jvmref ∧ (∀ rk. rk ∈ st → rk .ref ≠ r);
      is_a_newref :  ⊦ is_a_newref(r, st) ↔ r ≠ jvmref ∧ ¬ r ∈ st;
      is_the_newref :  ⊦ is_the_newref(r, st) ↔ r = newref(st);
      list_ok :  ⊦ is_newref_list(refs, st) ↔ ¬ dups(refs) ∧ (∀ r. r ∈ refs → newref(r, st));
      deleteref :  ⊦ ¬ r ∈ st -- r ∧ (∀ r0, sk. r ≠ r0 → (r0 -- sk ∈ st ↔ r0 -- sk ∈ st -- r) ∧ st[r0 -- sk] = (st -- r)[r0 -- sk]);
      catch-break :  ⊦ catch_break(st) = ((st[_mode] = break(`' .label) ⊃ st[_mode, noval]; st));
      catch-continue :  ⊦ catch_continue(st) = ((st[_mode] = continue(`' .label) ⊃ st[_mode, noval]; st));
      jump :  ⊦ jump(st) ↔ _mode ∈ st ∧ ¬ is_normal_mode(st[_mode]);
      normalmode :  ⊦ normalmode(st) ↔ _mode ∈ st ∧ st[_mode] = noval;
      out :  ⊦ _out(st) = flatten(st[_out]);
      used for : s, ls;
       
      newref-fun :  ⊦ newref(st) = next(maxref(st));
      newrefs-zero :  ⊦ newref_list(0, st) = [];
      newrefs-succ :  ⊦ newref_list(n + 1, st) = newref(st) + newref_list(n, st[newref(st) -- 0 ', noval]);
      maxref-empty :  ⊦ ¬ (∃ r. r ∈ st) → maxref(st) = jvmref;
      maxref-ok :  ⊦ r ∈ st → maxref(st) ∈ st ∧ (∀ r. r ∈ st → ¬ maxref(st) < r);
      initerror :  ⊦ initerror(class1, st) ↔ (jvmref -- mkfs(class1, void_type, `initstate' .field) ') × initval(error) ∈ st;
      used for : ls;
       
      initundone
      : ⊦ 
          initundone(class1, st)
        ↔   (jvmref -- mkfs(class1, void_type, `initstate' .field) ') × initval(undone) ∈ st
          ∨ ¬ jvmref -- mkfs(class1, void_type, `initstate' .field) ' ∈ st ∧ _uninit ∈ st;
      used for : ls;
       
      initdone :  ⊦ initdone(class1, st) ↔ ¬ initerror(class1, st) ∧ ¬ initundone(class1, st);
      used for : ls;
       
      initdoneP :  ⊦ initdoneP(class, st) ↔ is_predefined_class(class) ∨ initdone(class, st);
      used for : s, ls;
       
      initundoneP :  ⊦ initundoneP(class, st) ↔ ¬ is_predefined_class(class) ∧ initundone(class, st);
      used for : s, ls;
       
      init :  ⊦ init(st) ↔ (∀ class1. initdone(class1, st));
      comment: hierarchy persistent. Check that no `initstate'-field exists in store,
                   and that _uninit not in store;
       
      init-existing :  ⊦ init(str, st) ↔ (∀ class. tdname∃(str, class) → initdone(class, st));
      uninit :  ⊦ uninit(st) ↔ (∀ class1. initundone(class1, st));
      comment: hierarchy persistent. Check that no `initstate'-field, 
                   but _uninit exists in store;
       
      uninit-existing :  ⊦ uninit(str, st) ↔ (∀ class. tdname∃(str, class) → initundone(class, st));
end enrich