enrich fieldinit , 
       storearrays with
   functions 
      update : reference × fieldinits × store → store;
       . .keys : fieldinits → storekeys;
       . .vals : fieldinits → javavalues;
   predicates 
      validFields : reference × fieldinits × store;
      okValues : reference × fieldinits × store;
      hasKeys : reference × storekeys × store;
      validFieldValues : reference × storekeys × store;
      validFieldValue : reference × storekey × store;
      eqref : reference × reference × store × store;
      eqval : javavalue × javavalue × store × store;
      is_javastore : store;
      okstore : store;
      comment: mode/out in store, every ref has a type;
       
      okclass : javavalue × classname × store;
      comment: every ref is <= class;
       
      okreftype : javavalue × javatype × store;
      comment: null allowed, uses ≤;
       
      exactreftype : javavalue × javatype × store;
      oktype : javavalue × javatype × store;
      exacttype : javavalue × javatype × store;
      goodfieldandtype : reference × storekey × store;
      goodfieldsandtypes : reference × storekeys × store;
      exactfieldandtype : reference × storekey × store;
      exactfieldsandtypes : reference × storekeys × store;
       . ∈ . : fieldinits × store;
      instore : reference × classname × fieldinits × store;
      oksubtype : javavalue × classname × store;
      asgcomp : string × javavalue × javatype × store;
      is_array : reference × store;
      comment: true if the reference points to an array.
                                     This is comparable to is_obj in addfuns.;
       
      is_array : string × reference × store;
      comment: true if the reference points to an array with a 'good' element type.
                                     A good element type must exist, and may not be void or abstract.;
       
      okarray : reference × javatype × store;
      okarray : javavalue × javatype × int × store;
      exactarray : reference × javatype × store;
      exactarray : javavalue × javatype × int × store;
      okbytearray : reference × store;
      okarraytype : javavalue × javatype × store;
      okarrays : reference × fieldinits × store;
   
   axioms 
      asgcomp :  ⊦ asgcomp(str, val, ty, st) ↔ ¬ is_referencevalue(val) ∨ val .refval = jvmref ∨ is_subtype(str, st[val .refval -- _type] .type, ty);
      used for : s, ls;
       
      oksubtype
      : ⊦ 
          oksubtype(val, class, st)
        ↔ reftypep(val, st) ∧ (val .refval ≠ jvmref → val .refval -- _type ∈ st ∧ st[val .refval -- _type] .type .class ≤ class);
      used for : ls;
       
      update-empty :  ⊦ update(r, [], st) = st;
      used for : s, ls;
       
      update-rec :  ⊦ update(r, (sk × val) ' + fis, st) = (update(r, fis, st)[r -- sk, val]);
      used for : ls;
       
      getkeys-empty :  ⊦ [] .keys = [];
      used for : s, ls;
       
      getkeys-rec :  ⊦ ((sk × val) ' + fis) .keys = sk ' + fis .keys;
      used for : s, ls;
       
      getvals-empty :  ⊦ [] .vals = [];
      used for : s, ls;
       
      getvals-rec :  ⊦ ((sk × val) ' + fis) .vals = val ' + fis .vals;
      used for : s, ls;
       
      validFields :  ⊦ validFields(r, fis, st) ↔ unique_al(fis) ∧ ¬ _type ∈ fis ∧ ¬ _length ∈ fis ∧ hasKeys(r, fis .keys, st);
      hasKeys-empty :  ⊦ hasKeys(r, [], st);
      used for : s, ls;
       
      hasKeys-rec :  ⊦ hasKeys(r, sk ' + sks, st) ↔ r -- sk ∈ st ∧ hasKeys(r, sks, st);
      used for : ls;
       
      instore-empty :  ⊦ instore(r, class, [], st) ↔ r ≠ jvmref ∧ r -- _type ∈ st ∧ st[r -- _type] = typeval(mkclasstype(class));
      instore-rec :  ⊦ instore(r, class, (sk × val) ' + fis, st) ↔ (r -- sk) × val ∈ st ∧ instore(r, class, fis, st);
      is_javastore :  ⊦ is_javastore(st) ↔ _mode ∈ st ∧ _out ∈ st;
      okstore :  ⊦ okstore(st) ↔ is_javastore(st) ∧ (∀ r. r ≠ jvmref ∧ r ∈ st → r -- _type ∈ st ∧ is_typevalue(st[r -- _type]));
      okclass
      : ⊦ 
          okclass(val, class1, st)
        ↔ reftypep(val, st) ∧ (val .refval ≠ jvmref → val .refval -- _type ∈ st ∧ st[val .refval -- _type] = typeval(mkclasstype(class1)));
      used for : ls;
       
      okreftype
      : ⊦ 
          okreftype(val, ty, st)
        ↔   is_referencevalue(val)
          ∧ (val .refval ≠ jvmref → val .refval -- _type ∈ st ∧ is_typevalue(st[val .refval -- _type]) ∧ st[val .refval -- _type] .type ≤ ty);
      used for : ls;
       
      exactreftype
      : ⊦ 
          exactreftype(val, ty, st)
        ↔   is_referencevalue(val) ∧ val .refval ∈ st
          ∧ (val .refval ≠ jvmref → val .refval -- _type ∈ st ∧ is_typevalue(st[val .refval -- _type]) ∧ st[val .refval -- _type] .type = ty);
      used for : ls;
       
      validFieldValues-def :  ⊦ validFieldValues(r, sks, st) ↔ (∀ sk. sk ∈ sks → validFieldValue(r, sk, st));
      validFieldValue-def :  ⊦ validFieldValue(r, sk, st) ↔ is_fskey(sk) ∧ r -- sk ∈ st ∧ okval(st[r -- sk], sk .fs .type);
      used for : s, ls;
       
      good-base :  ⊦ goodfieldsandtypes(r, [], st);
      used for : s, ls;
       
      good-rec :  ⊦ goodfieldsandtypes(r, sk ' + sks, st) ↔ goodfieldandtype(r, sk, st) ∧ goodfieldsandtypes(r, sks, st);
      used for : ls;
       
      good-field
      : ⊦ 
          goodfieldandtype(r, mkfs(class1, ty, fieldvar) ', st)
        ↔ r -- mkfs(class1, ty, fieldvar) ' ∈ st ∧ oktype(st[r -- mkfs(class1, ty, fieldvar) '], ty, st);
      used for : ls;
       
      good-index :  ⊦ ¬ goodfieldandtype(r, i ', st);
      used for : s, ls;
       
      exact-base :  ⊦ exactfieldsandtypes(r, [], st);
      used for : s, ls;
       
      exact-rec :  ⊦ exactfieldsandtypes(r, sk ' + sks, st) ↔ exactfieldandtype(r, sk, st) ∧ exactfieldsandtypes(r, sks, st);
      used for : ls;
       
      exact-field
      : ⊦ 
          exactfieldandtype(r, mkfs(class1, ty, fieldvar) ', st)
        ↔ r -- mkfs(class1, ty, fieldvar) ' ∈ st ∧ exacttype(st[r -- mkfs(class1, ty, fieldvar) '], ty, st);
      used for : ls;
       
      exact-index :  ⊦ ¬ exactfieldandtype(r, i ', st);
      used for : s, ls;
       
      oktype-bool :  ⊦ oktype(val, boolean_type, st) ↔ is_boolvalue(val);
      used for : s, ls;
       
      oktype-int :  ⊦ oktype(val, int_type, st) ↔ is_integervalue(val);
      used for : s, ls;
       
      oktype-short :  ⊦ oktype(val, short_type, st) ↔ is_shortvalue(val);
      used for : s, ls;
       
      oktype-byte :  ⊦ oktype(val, byte_type, st) ↔ is_bytevalue(val);
      used for : s, ls;
       
      oktype-long :  ⊦ oktype(val, long_type, st) ↔ is_longvalue(val);
      used for : s, ls;
       
      oktype-char :  ⊦ oktype(val, char_type, st) ↔ is_charvalue(val);
      used for : s, ls;
       
      oktype-float :  ⊦ oktype(val, float_type, st) ↔ is_floatvalue(val);
      used for : s, ls;
       
      oktype-double :  ⊦ oktype(val, double_type, st) ↔ is_doublevalue(val);
      used for : s, ls;
       
      oktype-class :  ⊦ oktype(val, mkclasstype(class1), st) ↔ is_referencevalue(val);
      used for : ls;
       
      oktype-array :  ⊦ oktype(val, mkarraytype(ty), st) ↔ is_referencevalue(val);
      used for : ls;
       
      oktype-void :  ⊦ oktype(val, void_type, st) ↔ is_referencevalue(val);
      comment: identical to okval in valuefuns: null has void_type.;
      used for : s, ls;
       
      oktype-abstract :  ⊦ ¬ oktype(val, abstract_type, st);
      used for : s, ls;
       
      exacttype-bool :  ⊦ exacttype(val, boolean_type, st) ↔ is_boolvalue(val);
      used for : ls;
       
      exacttype-int :  ⊦ exacttype(val, int_type, st) ↔ is_integervalue(val);
      used for : ls;
       
      exacttype-short :  ⊦ exacttype(val, short_type, st) ↔ is_shortvalue(val);
      used for : ls;
       
      exacttype-byte :  ⊦ exacttype(val, byte_type, st) ↔ is_bytevalue(val);
      used for : ls;
       
      exacttype-class :  ⊦ exacttype(val, mkclasstype(class1), st) ↔ okclass(val, class1, st);
      used for : ls;
       
      exacttype-array :  ⊦ exacttype(val, mkarraytype(ty), st) ↔ exactreftype(val, mkarraytype(ty), st);
      used for : ls;
       
      exacttype-void :  ⊦ exacttype(val, void_type, st);
      used for : s, ls;
       
      exacttype-abstract :  ⊦ exacttype(val, abstract_type, st);
      used for : s, ls;
       
      instore-base :  ⊦ [] ∈ st;
      used for : s, ls;
       
      instore-rec :  ⊦ (sk × val) ' + fis ∈ st ↔ (jvmref -- sk) × val ∈ st ∧ fis ∈ st;
      used for : ls;
       
      exactarray
      : ⊦ 
          exactarray(r, ty, st)
        ↔   exactreftype(refval(r), mkarraytype(ty), st) ∧ r ≠ jvmref ∧ r -- _length ∈ st ∧ is_integervalue(st[r -- _length])
          ∧ 0 ≤ st[r -- _length] .intval ∧ is_arrayref(r, st[r -- _length] .intval, st);
      comment: ty is the element type, not the array type.;
       
      exactarray
      : ⊦ 
          exactarray(val, ty, i, st)
        ↔ exactreftype(val, mkarraytype(ty), st) ∧ val .refval ≠ jvmref ∧ (val .refval -- _length) × intval(i) ∈ st ∧ is_arrayref(val .refval, i, st);
      comment: ty is the element type, not the array type.;
       
      okarraytype :  ⊦ okarraytype(val, ty, st) ↔ is_referencevalue(val) ∧ (val .refval ≠ jvmref → okarray(val .refval, ty, st));
      comment: ty is the element type, not the array type.;
       
      is-any-array
      : ⊦ 
          is_array(r, st)
        ↔   r ≠ jvmref ∧ r -- _type ∈ st ∧ is_typevalue(st[r -- _type]) ∧ is_arraytype(st[r -- _type] .type)
          ∧ okarray(r, st[r -- _type] .type .type, st);
      is-real-array-def
      : ⊦ 
          is_array(str, r, st)
        ↔   type∃(str, st[r -- _type] .type) ∧ st[r -- _type] .type .jtelemtype ≠ void_type ∧ st[r -- _type] .type .jtelemtype ≠ abstract_type
          ∧ is_array(r, st);
      okarrayNotNull
      : ⊦ 
          okarray(r, ty, st)
        ↔   okreftype(refval(r), mkarraytype(ty), st) ∧ r ≠ jvmref ∧ 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 → oktype(st[r -- j '], ty, st));
      comment: ty is the element type, not the array type.;
       
      okarrayOfLength
      : ⊦ 
          okarray(val, ty, i, st)
        ↔   okreftype(val, mkarraytype(ty), st) ∧ val .refval ≠ jvmref ∧ (val .refval -- _length) × intval(i) ∈ st ∧ 0 ≤ i
          ∧ is_arrayref(val .refval, i, st) ∧ (∀ j. 0 ≤ j ∧ j < i → oktype(st[val .refval -- j '], ty, st));
      comment: ty is the element type, not the array type.;
       
      okarrays-base :  ⊦ okarrays(r, [], st);
      used for : s, ls;
       
      okarrays-rec
      : ⊦ 
          okarrays(r, (sk × val) ' + fis, st)
        ↔   is_integervalue(val) ∧ is_fskey(sk) ∧ is_arraytype(sk .fs .type) ∧ okarray(st[r -- sk], sk .fs .type .type, val .intval, st)
          ∧ okarrays(r, fis, st);
      okbytearray :  ⊦ okbytearray(r, st) ↔ okarray(r, byte_type, st);
      eqref
      : ⊦ 
          eqref(r, r0, st, st0)
        ↔   r = jvmref ∧ r0 = jvmref
          ∨ r ≠ jvmref ∧ r0 ≠ jvmref ∧ (∀ sk. (r -- sk ∈ st ↔ r0 -- sk ∈ st0) ∧ (r -- sk ∈ st → eqval(st[r -- sk], st0[r0 -- sk], st, st0)));
      eqval-intl :  ⊦ is_integervalue(val) → (eqval(val, val0, st, st0) ↔ val = val0);
      used for : s, ls;
       
      eqval-intr :  ⊦ is_integervalue(val0) → (eqval(val, val0, st, st0) ↔ val = val0);
      used for : s, ls;
       
      eqval-bytel :  ⊦ is_bytevalue(val) → (eqval(val, val0, st, st0) ↔ val = val0);
      used for : s, ls;
       
      eqval-byter :  ⊦ is_bytevalue(val0) → (eqval(val, val0, st, st0) ↔ val = val0);
      used for : s, ls;
       
      eqval-shortl :  ⊦ is_shortvalue(val) → (eqval(val, val0, st, st0) ↔ val = val0);
      used for : s, ls;
       
      eqval-shortr :  ⊦ is_shortvalue(val0) → (eqval(val, val0, st, st0) ↔ val = val0);
      used for : s, ls;
       
      eqval-booll :  ⊦ is_boolvalue(val) → (eqval(val, val0, st, st0) ↔ val = val0);
      used for : s, ls;
       
      eqval-boolr :  ⊦ is_boolvalue(val0) → (eqval(val, val0, st, st0) ↔ val = val0);
      used for : s, ls;
       
      eqval-refl :  ⊦ is_referencevalue(val) → (eqval(val, val0, st, st0) ↔ is_referencevalue(val0) ∧ eqref(val .refval, val0 .refval, st, st0));
      used for : s, ls;
       
      eqval-refr :  ⊦ is_referencevalue(val0) → (eqval(val, val0, st, st0) ↔ is_referencevalue(val) ∧ eqref(val .refval, val0 .refval, st, st0));
      used for : s, ls;
       
      eqval-concl
      : ⊦ 
          is_valuelist(val)
        → (  eqval(val, val0, st, st0)
           ↔ is_valuelist(val0) ∧ eqval(val .firstval, val0 .firstval, st, st0) ∧ eqval(val .restval, val0 .restval, st, st0));
      used for : s, ls;
       
      eqval-concr
      : ⊦ 
          is_valuelist(val0)
        → (  eqval(val, val0, st, st0)
           ↔ is_valuelist(val) ∧ eqval(val .firstval, val0 .firstval, st, st0) ∧ eqval(val .restval, val0 .restval, st, st0));
      used for : ls;
       
      eqval-novall :  ⊦ is_novalue(val) → (eqval(val, val0, st, st0) ↔ val = val0);
      used for : s, ls;
       
      eqval-novalr :  ⊦ is_novalue(val0) → (eqval(val, val0, st, st0) ↔ val = val0);
      used for : s, ls;
       
      eqval-typel :  ⊦ is_typevalue(val) → (eqval(val, val0, st, st0) ↔ val = val0);
      used for : s, ls;
       
      eqval-typer :  ⊦ is_typevalue(val0) → (eqval(val, val0, st, st0) ↔ val = val0);
      used for : s, ls;
       
      eqval-initl :  ⊦ is_initvalue(val) → (eqval(val, val0, st, st0) ↔ val = val0);
      used for : s, ls;
       
      eqval-initr :  ⊦ is_initvalue(val0) → (eqval(val, val0, st, st0) ↔ val = val0);
      used for : s, ls;
       
      eqval-breakl :  ⊦ is_break_mode(val) → (eqval(val, val0, st, st0) ↔ val = val0);
      used for : s, ls;
       
      eqval-breakr :  ⊦ is_break_mode(val0) → (eqval(val, val0, st, st0) ↔ val = val0);
      used for : s, ls;
       
      eqval-continuel :  ⊦ is_continue_mode(val) → (eqval(val, val0, st, st0) ↔ val = val0);
      used for : s, ls;
       
      eqval-continuer :  ⊦ is_continue_mode(val0) → (eqval(val, val0, st, st0) ↔ val = val0);
      used for : s, ls;
       
      eqval-returnl :  ⊦ is_return_mode(val) → (eqval(val, val0, st, st0) ↔ val = val0);
      used for : s, ls;
       
      eqval-returnr :  ⊦ is_return_mode(val0) → (eqval(val, val0, st, st0) ↔ val = val0);
      used for : s, ls;
       
      eqval-throwl :  ⊦ is_throw_mode(val) → (eqval(val, val0, st, st0) ↔ val = val0);
      used for : s, ls;
       
      eqval-throwr :  ⊦ is_throw_mode(val0) → (eqval(val, val0, st, st0) ↔ val = val0);
      used for : s, ls;
       
end enrich