enrich multiarrays with
   predicates 
      junkrefs : string × javavalues × store;
      comment: true if one value is a junkref.;
       
      junkref : string × reference × store;
      comment: true if the reference points
                        to a non-valid pointer structure.;
       
      junkrefs : string × references × javatype × store;
      validref : string × reference × javatype × store;
      comment: null allowed, uses ≤,
                                                         uses junkref(s);
       
      validreflist : string × javavalues × javatype × store;
      comment: all validref.;
       
      validfield : string × reference × storekey × store;
      comment: good field, and if
                    a reference, then valid.;
       
      validfieldlist : string × reference × storekeys × store;
      comment: all fields
                        goodfieldandtype, and ref's are validref.;
       
      validrefnotnull : string × reference × javatype × store;
      validrefvalnotnull : string × javavalue × javatype × store;
      validrefval : string × javavalue × javatype × store;
      comment: val is a ref and validref.;
       
      validrefkeynotnull : string × refkey × javatype × store;
      validval : string × javavalue × javatype × store;
      comment: val is okval, and validref if a reference.;
       
      validval : string × refkey × javavalue × store;
      validvals : string × refkeyvalues × store;
      validfieldinits : string × fieldinits × store;
      validstatfields : string × store;
      comment: true if all statfields of all
                                         initialized classes are validrefs.;
       
      validstatfields : string × classname × store;
      comment: true if all statfields of 
                                                     this class are validrefs.;
       
      validstatfields : string × storekeys × store;
      comment: true if all sk ∈ storekeys, which are statfields of initialized classes, 
                                  are validfield;
       
      validstatfield : string × storekey × store;
      comment: true if sk is a statfield, and (if initialized) is a validfield;
       
      validmode : string × store;
      comment: true if mode field contains a valid entry.;
       
      validmode : string × javavalue × store;
      comment: auxiliary for validmode above.;
       
      valid⊆ : string × store × store;
      comment: see java-all/junkref. 
                   valid⊆(str, st, st0): All validref's in st stay valid in st0, all
                                         new refs in st0 (not in st) are validrefs.;
       
      init⊆ : string × store × store;
      comment: see java-all/junkref. 
                   init⊆(str, st, st0): All valid static fields in st remain valid in st0,
                                        For newly initialized classes (initdone in st0, but
                                        not in st) all static fields are valid.;
       
      level⊆ : string × string;
      comment: level⊆(str, str0): all classes and interfaces
                                    of level str also exist in str0, i.e. str is a subspec of str0.;
       
      same-subclasses : classname × string × string;
      comment: same-subclasses(class, str, str0): 
                                class has the same subclasses at level str0 as at level str.;
       
   
   axioms 
      junkreflist-def :  ⊦ junkrefs(str, vals, st) ↔ (∃ r. refval(r) ∈ vals ∧ junkref(str, r, st));
      junkref-def :  ⊦ junkref(str, r, st) ↔ (∃ refs. refs ≠ [] ∧ refs .first = r ∧ junkrefs(str, refs, st[r -- _type] .type, st));
      junkrefs-empty :  ⊦ ¬ junkrefs(str, [], ty, st);
      used for : s, ls;
       
      junkrefs-null :  ⊦ r = jvmref → ¬ junkrefs(str, r ' + refs, ty, st);
      junkrefs-is-junk :  ⊦ r ≠ jvmref ∧ (¬ is_valid_ref(str, r, st) ∨ ¬ st[r -- _type] .type ≤ ty) → junkrefs(str, r ' + refs, ty, st);
      junkrefs-class
      : ⊦ 
          is_obj(str, r, st) ∧ st[r -- _type] .type ≤ ty
        → (  junkrefs(str, r ' + refs, ty, st)
           ↔   refs ≠ []
             ∧ (∃ fs. 
                   fs ' ∈ instfields(st[r -- _type] .type .class) ∧ is_referencevalue(st[r -- fs ']) ∧ refs .first = st[r -- fs '] .refval
                 ∧ junkrefs(str, refs, fs .type, st)));
      junkrefs-array
      : ⊦ 
          is_array(str, r, st) ∧ st[r -- _type] .type ≤ ty
        → (  junkrefs(str, r ' + refs, ty, st)
           ↔   refs ≠ []
             ∧ (∃ i. 
                   0 ≤ i ∧ i < st[r -- _length] .intval ∧ is_referencevalue(st[r -- i ']) ∧ refs .first = st[r -- i '] .refval
                 ∧ junkrefs(str, refs, st[r -- _type] .type .type, st)));
      validref-def :  ⊦ validref(str, r, ty, st) ↔ r = jvmref ∨ st[r -- _type] .type ≤ ty ∧ ¬ junkref(str, r, st);
      validreflist-def :  ⊦ validreflist(str, vals, ty, st) ↔ (∀ val. val ∈ vals → is_referencevalue(val) ∧ validref(str, val .refval, ty, st));
      comment: useful for adding arrays with reference types.;
       
      validfield-def
      : ⊦ 
          validfield(str, r, sk, st)
        ↔   goodfieldandtype(r, sk, st) ∧ type∃(str, sk .fs .type) ∧ sk .fs .type ≠ void_type
          ∧ (is_reftype(sk .fs .type) → validrefval(str, st[r -- sk], sk .fs .type, st));
      validfieldlist-def :  ⊦ validfieldlist(str, r, sks, st) ↔ (∀ sk. sk ∈ sks → validfield(str, r, sk, st));
      validrefkeynotnull-def :  ⊦ validrefkeynotnull(str, rk, ty, st) ↔ rk ∈ st ∧ validrefvalnotnull(str, st[rk], ty, st);
      validrefvalnotnull-def :  ⊦ validrefvalnotnull(str, val, ty, st) ↔ is_referencevalue(val) ∧ validrefnotnull(str, val .refval, ty, st);
      validrefval-def :  ⊦ validrefval(str, val, ty, st) ↔ is_referencevalue(val) ∧ validref(str, val .refval, ty, st);
      validrefnotnull-def :  ⊦ validrefnotnull(str, r, ty, st) ↔ r ≠ jvmref ∧ validref(str, r, ty, st);
      validval-def :  ⊦ validval(str, val, ty, st) ↔ okval(val, ty) ∧ (is_referencevalue(val) → validrefval(str, val, ty, st));
      validrefkeyval-def
      : ⊦ 
          validval(str, r -- sk, val, st)
        ↔   (is_fskey(sk) → validval(str, val, sk .fs .type, st) ∧ sk .fs .type ≠ void_type ∧ sk ≠ _length)
          ∧ (is_indexkey(sk) → validval(str, val, st[r -- _type] .type .type, st));
      validrefkeyvalues-def :  ⊦ validvals(str, rkvs, st) ↔ (∀ rkv. rkv ∈ rkvs → validval(str, rkv .1, rkv .2, st));
      validfieldinits-def
      : ⊦ 
        validfieldinits(str, fis, st) ↔ (∀ sk, val. sk × val ∈ fis → is_fskey(sk) ∧ type∃(str, sk .fs .type) ∧ validval(str, val, sk .fs .type, st));
      validstatfields-def
      :  ⊦ validstatfields(str, st) ↔ (∀ class. tdname∃(str, class) ∧ initdone(class, st) → validfieldlist(str, jvmref, statfields(class), st));
      validstatfields-class :  ⊦ validstatfields(str, class, st) ↔ validfieldlist(str, jvmref, statfields(class), st);
      validstatfield-storekey-def
      : ⊦ 
          validstatfield(str, sk, st)
        ↔   is_fskey(sk) ∧ sk ∈ statfields(sk .fs .class) ∧ tdname∃(str, sk .fs .class)
          ∧ (initdone(sk .fs .class, st) → validfield(str, jvmref, sk, st));
      validstatfields-storekeys-def :  ⊦ validstatfields(str, sks, st) ↔ (∀ sk. sk ∈ sks → validstatfield(str, sk, st));
      validmode-def :  ⊦ validmode(str, st) ↔ _mode ∈ st ∧ validmode(str, st[_mode], st);
      validmodeval-def
      : ⊦ 
          validmode(str, val, st)
        ↔   val = noval ∨ is_break_mode(val) ∨ val = return(noval, void_type) ∨ is_return_mode(val) ∧ validref(str, val .refval, val .type, st)
          ∨   is_throw_mode(val) ∧ val .refval ≠ jvmref ∧ validref(str, val .refval, val .type, st)
            ∧ val .type ≤ mkclasstype(`java.lang.Throwable' .class);
      validsubset-def
      :  ⊦ valid⊆(str, st, st0) ↔ (∀ r, ty. validref(str, r, ty, st) → validref(str, r, ty, st0)) ∧ (∀ r. ¬ r ∈ st ∧ r ∈ st0 → ¬ junkref(str, r, st0));
      initsubset-def
      : ⊦ 
          init⊆(str, st, st0)
        ↔   (∀ class. initdone(class, st) → initdone(class, st0)) ∧ (∀ class. initerror(class, st) → initerror(class, st0))
          ∧ (∀ class. ¬ initdone(class, st) ∧ initdone(class, st0) ∧ tdname∃(str, class) → validstatfields(str, statfields(class), st0))
          ∧ (∀ class, sk. 
                initdone(class, st) ∧ initdone(class, st0) ∧ tdname∃(str, class) ∧ sk ∈ statfields(class) ∧ validstatfield(str, sk, st)
              → validstatfield(str, sk, st0));
      levelsubset-def
      :  ⊦ level⊆(str, str0) ↔ (∀ class. class∃(str, class) → class∃(str0, class)) ∧ (∀ class. interface∃(str, class) → interface∃(str0, class));
      same-subclasses-one-def
      : ⊦ 
          same-subclasses(class, str, str0)
        ↔   (∀ class0. class∃(str0, class0) ∧ class0 ≤ class → class∃(str, class0))
          ∧ (∀ class0. interface∃(str0, class0) ∧ class0 ≤ class → interface∃(str, class0));
end enrich