[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,
enrich addarray with
functions
addarrays : references × javatype × intlist × int × store → store;
comment: creates a multi-dimensional array, i.e. an array of arrays
of arrays etc.
references is a list of all needed (new) references that will be used
for the toplevel array and subarrays.
javatype is the innermost element type ty as given in the
new ty[3][5][] expression.
intlist the explicitly given dimensions, e.g. [3][5].
int extra dimensions, i.e. +1 for every [].
store the store.
;
addmultiarrays : references × int × references × javatype × intlist × store → store;
comment: auxiliary function for addarrays.
;
addarraymult : reference × javatype × store × references × intlist × int → store;
addarraymultlist : reference × javatype × store × references × intlist × intlist × int → store;
comment: addarraymultlist(r,ty,st,refs,ints,ints0, i) adds a
multidimensional array for reference r with final element type
ty to store st.
ints are the dimensions and are used as index variables, i.e.
they run from their initial length down to 0.
ints0 are the lengths of the arrays (initially equal to ints).
refs is a list of (new) references for the subarrays. It's
initial length must be countrefs(ints0).
The final int i is the number of further
dimensions (needed to determine the initial value).;
countrefs : intlist → int;
countrefs2 : intlist → int;
countdims : intlist × int → int;
getdims : intlist → intlist;
ints# : intlist → nat;
variables
acc : references;
axioms
countrefs-base : ⊦ # ints ≤ 1 → countrefs(ints) = 1;
countrefs-zero : ⊦ # ints > 1 ∧ ints .first ≤ 0 → countrefs(ints) = 1;
countrefs-rec : ⊦ # ints > 1 ∧ ints .first > 0 → countrefs(ints) = 1 + ints .first * countrefs(ints .rest);
countdims-empty : ⊦ countdims([], i) = i;
used for : s, ls;
countdims-zero : ⊦ j ≤ 0 → countdims(j ' + ints, i) = i + n→i(# ints);
used for : s, ls;
countdims-rec : ⊦ 0 < j → countdims(j ' + ints, i) = countdims(ints, i);
used for : s, ls;
getdims-empty : ⊦ getdims([]) = [];
used for : s, ls;
getdims-zero : ⊦ j ≤ 0 → getdims(j ' + ints) = 0 ';
used for : s, ls;
getdims-rec : ⊦ 0 < j → getdims(j ' + ints) = j ' + getdims(ints);
used for : s, ls;
addarrays-def
: ⊦
ints ≠ [] ∧ n→i(# refs) = countrefs(ints) ∧ posints(ints)
→ addarrays(refs, ty, ints, i, st) = addmultiarrays(refs, ints .first, [], mktype_from_dims(ty, countdims(ints, i)), getdims(ints), st);
addarrays-empty : ⊦ ints = [] ∨ n→i(# refs) ≠ countrefs(ints) ∨ ¬ posints(ints) → addarrays(refs, ty, ints, i, st) = st;
addmultiarrays-base : ⊦ # ints = 1 → addmultiarrays(refs, i, acc, ty, ints, st) = addarray(refs .first, ty, ints .first, st);
addmultiarrays-done
: ⊦
i = 0 ∧ # ints > 1
→ addmultiarrays(refs, i, acc, ty, ints, st) = addarray(refs .first, mktype_from_dims(ty, n→i(# ints) - 1), mkjavavalues(acc), st);
addmultiarrays-rec
: ⊦
i > 0 ∧ # ints > 1
→ addmultiarrays(refs, i, acc, ty, ints, st)
= addmultiarrays
(firstn(# refs - i→n(countrefs(ints .rest)), refs), i - 1, lastn(i→n(countrefs(ints .rest)), refs) .first + acc, ty, ints,
addmultiarrays(lastn(i→n(countrefs(ints .rest)), refs), ints .rest .first, [], ty, ints .rest, st));
addarraymult : ⊦ addarraymult(r, ty, st, refs, ints, i) = addarraymultlist(r, ty, st, refs, ints, ints, i);
used for : s, ls;
addarraymultlist_zero : ⊦ # ints = 0 → addarraymultlist(r, ty, st, refs, ints, ints0, i) = st;
comment: shouldn't occur, just to specify every case;
used for : ls;
addarraymultlist_one_0
: ⊦
# ints = 1 ∧ ints .first ≤ 0
→ addarraymultlist(r, ty, st, refs, ints, ints0, i)
= (st[r -- _type, typeval(mktype_from_dims(ty, n→i(# ints) + i))][r -- _length, intval(ints0 .first)]);
comment: add(r,ty,st,refs, [0], ints0, i)
one array of length 0 - it's possible;
addarraymultlist_one_not_0
: ⊦ # ints = 1 ∧ ints .first > 0 → addarraymultlist(r, ty, st, refs, ints, ints0, i) = addarray(r, mktype_from_dims(ty, i), ints0 .first, st);
comment: add(r,ty,st,refs, [n +1], ints0, i) = one array of length n +1;
addarraymultlist_more_0
: ⊦
# ints > 1 ∧ ints .first ≤ 0
→ addarraymultlist(r, ty, st, refs, ints, ints0, i)
= (st[r -- _type, typeval(mktype_from_dims(ty, n→i(# ints) + i))][r -- _length, intval(ints0 .first)]);
comment: add(r,ty,st,refs, [0, x], ints0, i) = one array of length 0, the
following expressions are discarded;
addarraymultlist_more_1
: ⊦
# ints > 1 ∧ ints .first = 1
→ addarraymultlist(r, ty, st, refs, ints, ints0, i)
= addarraymultlist
(refs .first, ty,
st[r -- (ints .first - 1) ', refval(refs .first)][r -- _type, typeval(mktype_from_dims(ty, i + n→i(# ints)))]
[r -- _length, intval(ints0 .first)
],
refs .rest, ints .rest, ints0 .rest, i);
comment: add(r,ty,st,refs, [1, x], ints0, i), just the outer recursion;
addarraymultlist_more_2
: ⊦
# ints > 1 ∧ ints .first ≥ 1 + 1
→ addarraymultlist(r, ty, st, refs, ints, ints0, i)
= addarraymultlist
(refs .first, ty,
addarraymultlist
(r, ty,
st[r -- (ints .first - 1) ', refval(refs .first)][r -- _type, typeval(mktype_from_dims(ty, i + n→i(# ints)))]
[r -- _length, intval(ints0 .first)
],
refs .rest, (ints .first - 1) + ints .rest, ints0, i),
restn(i→n(countrefs2((ints .first - 1) + ints .rest)), refs .rest), ints .rest, ints0 .rest, i);
comment: main recursion. add(r,ty,st,refs, [n +2, x], ints0, i) =
1. inner recursion: add(r,ty,st,refs, [n +1, x], ints0, i), i.e. create other
arrays
2. outer recursion: add(r,ty,st,refs, [x], ints0, i), i.e. add arrays for
index n +1
;
intssize-empty : ⊦ ints#([]) = 0;
used for : s, ls;
intssize-rec : ⊦ ints#(i ' + ints) = 1 + i→n(i) + ints#(ints);
used for : s, ls;
countrefs_one : ⊦ # ints ≤ 1 → countrefs2(ints) = 0;
countrefs_more_le0 : ⊦ # ints > 1 ∧ ints .first ≤ 0 → countrefs2(ints) = 0;
countrefs_more_gr0 : ⊦ # ints > 1 ∧ ints .first > 0 → countrefs2(ints) = ints .first + ints .first * countrefs2(ints .rest);
end enrich