enrich pointers with
comment: 
The following theorem used to hold, but junkref now forbids void and abstract arrays, and interfaces and
abstract classes.

compat-not-junkref :
⊦ 
compat(str, st) ∧ has_type(r, st) ∧ compat(str, refval(r), st[r -- _type] .type, st) → ¬ junkref(str, r, st), 

Proof: expand junkref to junkrefs and use induction on refs.
;
   predicates 
      compat : string × store;
      compatmode : string × store;
      compatmode : string × javavalue × store;
      compatstatic : string × store;
      comment: note:
                        ⊦ validstatfields(str, st) → compatstatic(str, st)
                        does not hold, because validstatfields allows 'objects' for an
                        interface type while compatstatic does not. ;
       
      compatrefs : string × store;
      compatobj : string × reference × store;
      compatarray : string × reference × store;
      comment: allows void and abstract arrays.;
       
      compatfields : string × reference × storekeys × store;
      compat : string × valuetypes × store;
      compat : string × javavalue × javatype × store;
      acyclic-ref : reference × store;
      comment: version with indet DL-program.;
       
      cyclic-ref : reference × store;
      comment: version with indet DL-program.;
       
      okpath : reference × store × references;
      comment: okpath(r,st,refs) ↔ es gibt pointerstruktur mit Wurzel
				r im Store, von der aus transitiv refs erreichbar sind;
       
   procedures 
      followRefs  reference × store :  nonfunctional nondeterministic;
   
   axioms 
      okpath-notin :  ⊦ ¬ r1 ∈ st → ¬ okpath(r, st, r1 + refs);
      okpath-empty :  ⊦ okpath(r, st, []);
      used for : s, ls;
       
      okpath-rec
      : ⊦ 
          typeval(ty) = st[r -- _type] ∧ is_classtype(ty)
        → (okpath(r, st, r0 + refs) ↔ (∃ fs. fs ' ∈ instfields(ty .class) ∧ st[r -- fs '] = refval(r0) ∧ okpath(r0, st, refs)));
      okpath-rec-array
      : ⊦ 
          typeval(ty) = st[r -- _type] ∧ is_arraytype(ty)
        → (okpath(r, st, r0 + refs) ↔ (∃ i. 0 ≤ i ∧ i < st[r -- _length] .intval ∧ st[r -- i '] = refval(r0) ∧ okpath(r0, st, refs)));
      acyclic-ref-def :  ⊦ acyclic-ref(r, st) ↔ ⟪followRefs(r, st)⟫ true;
      cyclic-ref-def :  ⊦ cyclic-ref(r, st) ↔ ¬ acyclic-ref(r, st);
      store-compat :  ⊦ compat(str, st) ↔ compatmode(str, st) ∧ compatstatic(str, st) ∧ compatrefs(str, st);
      mode-compat :  ⊦ compatmode(str, st) ↔ _mode ∈ st ∧ compatmode(str, st[_mode], st);
      modeval-compat
      : ⊦ 
          compatmode(str, val, st)
        ↔   val = noval ∨ is_break_mode(val) ∨ val = return(noval, void_type) ∨ is_return_mode(val) ∧ compat(str, val .val, val .type, st)
          ∨   is_throw_mode(val) ∧ val .refval ≠ jvmref ∧ compat(str, refval(val .refval), val .type, st)
            ∧ is_subtype(str, val .type, mkclasstype(`java.lang.Throwable' .class));
      static-compat
      :  ⊦ compatstatic(str, st) ↔ (∀ class. tdname∃(str, class) ∧ initdone(class, st) → compatfields(str, jvmref, statfields(class), st));
      refs-compat
      : ⊦ 
          compatrefs(str, st)
        ↔ (∀ r. 
              r ≠ jvmref ∧ r -- _type ∈ st ∧ is_typevalue(st[r -- _type])
            →   (is_classtype(st[r -- _type] .type) ∧ class+∃(str, st[r -- _type] .type .class) → compatobj(str, r, st))
              ∧ (    is_arraytype(st[r -- _type] .type)
                   ∧ (¬ has_classtype(st[r -- _type] .type) ∨ tdname+∃(str, st[r -- _type] .type .jtelemtype .class))
                 → compatarray(str, r, st)));
      obj-compat
      : ⊦ 
          compatobj(str, r, st)
        ↔   is_classtype(st[r -- _type] .type) ∧ class+∃(str, st[r -- _type] .type .class)
          ∧ compatfields(str, r, instfields(st[r -- _type] .type .class), st);
      fields-compat :  ⊦ compatfields(str, r, sks, st) ↔ (∀ sk. sk ∈ sks → r -- sk ∈ st ∧ is_fskey(sk) ∧ compat(str, st[r -- sk], sk .fs .type, st));
      value-compat
      : ⊦ 
          compat(str, val, ty, st)
        ↔   okval(val, ty)
          ∧ (  is_referencevalue(val) ∧ val .refval ≠ jvmref
             →   val .refval -- _type ∈ st ∧ is_typevalue(st[val .refval -- _type]) ∧ is_reftype(st[val .refval -- _type] .type)
               ∧ (has_classtype(st[val .refval -- _type] .type) → tdname+∃(str, st[val .refval -- _type] .type .jtelemtype .class))
               ∧ (is_classtype(st[val .refval -- _type] .type) → class+∃(str, st[val .refval -- _type] .type .class)) ∧ asgcomp(str, val, ty, st));
      array-compat
      : ⊦ 
          compatarray(str, r, st)
        ↔   is_arraytype(st[r -- _type] .type) ∧ r -- _length ∈ st ∧ is_integervalue(st[r -- _length]) ∧ 0 ≤ st[r -- _length] .intval
          ∧ is_arrayref(r, st[r -- _length] .intval, st)
          ∧ (∀ j. 0 ≤ j ∧ j < st[r -- _length] .intval → compat(str, st[r -- j '], st[r -- _type] .type .type, st));
      params-compat :  ⊦ compat(str, vts, st) ↔ (∀ vt. vt ∈ vts → compat(str, vt .val, vt .type, st));
declaration 
   followRefs (r, st)
     { 
        if ¬ r ∈ st ∨ r = jvmref
        then skip
        else if ∃ ty. 
                   typeval(ty) = st[r -- _type] ∧ is_classtype(ty) ∧ instfields(ty .class) ≠ []
                 ∧ (∃ fs. fs ' ∈ instfields(ty .class) ∧ (∃ r0. st[r -- fs '] = refval(r0)))
             then choose  fs, r0 with (fs ' ∈ instfields(st[r -- _type] .type .class) ∧ refval(r0) = st[r -- fs ']) in followRefs(r0, st)
             else if ∃ ty. 
                        typeval(ty) = st[r -- _type] ∧ is_arraytype(ty)
                      ∧ (∃ i. 0 ≤ i ∧ i < st[r -- _length] .intval ∧ (∃ r0. st[r -- i '] = refval(r0)))
                  then choose  i, r0 with (0 ≤ i ∧ i < st[r -- _length] .intval ∧ refval(r0) = st[r -- i ']) in followRefs(r0, st)
     };
end enrich