[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Specification addarray
enrich addfuns with
   functions 
      addarray : reference × javatype × int × store → store;
      comment: addarray(r,ty,i,st) adds an array for reference r with
                                  element(!) type ty of length i to store st;
       
      addarray : reference × javatype × javavalues × store → store;
      comment: addarray(r, ty, vals, st) adds an array for reference r
                                  with element(!) type ty and initial elements vals to
                                  store st. Do induction on # vals.
                         ;
       
      addarray : reference × javatype × bytelist × store → store;
      comment: as above, but add a byte array;
       
      addarray : reference × javavalue × int × store → store;
      comment: auxiliary function for addarray without initialization;
       
      addarray : reference × javavalues × int × store → store;
      comment: auxiliary function for addarray with initialization;
       
      addbytearray : reference × intlist × store → store;
   
   axioms 
      addarray-def :  ⊦ addarray(r, ty, i, st) = addarray(r, initial_value(ty), i, st[r -- _type, typeval(mkarraytype(ty))][r -- _length, intval(i)]);
      used for : ls;
       
      addarray-base :  ⊦ i ≤ 0 → addarray(r, val, i, st) = st;
      used for : ls;
       
      addarray-rec :  ⊦ i > 0 → addarray(r, val, i, st) = (addarray(r, val, i - 1, st)[r -- (i - 1) ', val]);
      addarrayinit-def
      :  ⊦ addarray(r, ty, vals, st) = addarray(r, vals, 0, st[r -- _type, typeval(mkarraytype(ty))][r -- _length, intval(n→i(# vals))]);
      used for : ls;
       
      addarrayinit-base :  ⊦ addarray(r, [], i, st) = st;
      used for : ls;
       
      addarrayinit-rec :  ⊦ addarray(r, val ' + vals, i, st) = (addarray(r, vals, i + 1, st)[r -- i ', val]);
      used for : ls;
       
      addbytearray :  ⊦ addarray(r, ty, bytes, st) = addarray(r, ty, mkjavavalues(bytes), st);
      used for : s, ls;
       
      addbytearray-ints :  ⊦ addbytearray(r, ints, st) = addarray(r, byte_type, mkjavavalues(is2bs(ints)), st);
end enrich