Atj-java-primitive-array-model
ATJ's model of Java primitive arrays.
For the purpose of generating Java code
that manipulates Java primitive arrays,
we introduce an ACL2 representation of Java primitive arrays
and of operations on such arrays.
This is currently not part of our Java language formalization,
but it may eventually be replaced with
a perhaps more general model from the Java language formalization.
The current model only serves ATJ's needs;
it is not meant to model all aspects of Java primitive arrays.
ATJ's use of this model of Java primitive arrays
is described in atj-java-primitive-arrays.
We model a Java primitive array essentially as
a list of Java primitive values whose length is below 2^{31}.
This length limit is derived from the fact that
the length field of an array has type int [JLS14:10.7],
and the maximum integer representable with int is 2^{31}-1.
We tag the list, via fty::defprod,
with an indication of the primitive types.
We introduce the following functions,
eight of each kind, for the eight Java primitive types:
- Operations to read components of Java primitive arrays:
these model array accesses whose results are used as values.
The index is (our ACL2 model of) a Java int,
and the result is (our ACL2 model of) the array component type.
- Operations to obtain the lengths of Java primitive arrays:
these model accesses of the length field of arrays.
The result is (our ACL2 model of) a Java int.
- Operations to write components of Java primitive arrays:
these model the assignment of values
to array access expressions whose results are used as variables
(these operations functionally return updated arrays).
The index is (our ACL2 model of) a Java int,
the new component value is (our ACL2 model of) the array component type,
and the result is the new Java primitive array.
- Operations to create new Java primitive arrays of given lengths
(and with every component the default value for the component type,
i.e. false for boolean and 0 for the integral types
[JLS14:4.12.5]):
these model array creation expressions
with lengths and without initializers.
The size is (our ACL2 model of) a Java int,
and the result is the newly created Java primitive array.
- Operations to create new Java primitive arrays with given components:
these model array creation expressions
without lengths and with initializers.
The inputs are lists of (our ACL2 models of) Java primitive values
(of the arrays' component types),
and the outputs are the newly created Java primitive arrays.
These operations are the same as the constructors of the array fixtypes,
but introducing them provides future flexibility,
should the definition of the fixtype change in some way.
- Operations to convert from Java primitive arrays to ACL2 lists,
component-wise:
a Java boolean array is converted to
the list of corresponding ACL2 booleanp values;
a Java char array is converted to
the list of corresponding ACL2 ubyte16p values;
a Java byte array is converted to
the list of corresponding ACL2 sbyte8p values;
a Java short array is converted to
the list of corresponding ACL2 sbyte16p values;
a Java int array is converted to
the list of corresponding ACL2 sbyte32p values; and
a Java long array is converted to
the list of corresponding ACL2 sbyte64p values.
No conversion operations for float and double arrays
are defined here,
because we have an abstract model of those two primitive types.
- Operations to convert to Java primitive arrays from ACL2 lists,
component-wise; these are the inverse conversions of
those described just above.
Note that the conversions between Java arrays and ACL2 lists
involve lists of ACL2 values, not of Java primitive values.
The reason is that ACL2 lists of (our model of) Java primitive values
do not really have a place in the generated Java code,
which separates Java primitive values and arrays from built-in ACL2 values,
through the ATJ types.
Subtopics
- Atj-def-java-primitive-array-model
- Macro to define the models of Java primitive arrays.
- Short-array
- Fixtype of (our model of) Java short arrays.
- Long-array
- Fixtype of (our model of) Java long arrays.
- Int-array
- Fixtype of (our model of) Java int arrays.
- Char-array
- Fixtype of (our model of) Java char arrays.
- Byte-array
- Fixtype of (our model of) Java byte arrays.
- Boolean-array
- Fixtype of (our model of) Java boolean arrays.
- Float-array
- Fixtype of (our model of) Java float arrays.
- Double-array
- Fixtype of (our model of) Java double arrays.
- Byte-array-to-sbyte8-list
- Convert a Java byte array to
an ACL2 list of signed 8-bit integers.
- Short-array-to-sbyte16-list
- Convert a Java short array to
an ACL2 list of signed 16-bit integers.
- Long-array-to-sbyte64-list
- Convert a Java long array to
an ACL2 list of signed 64-bit integers.
- Int-array-to-sbyte32-list
- Convert a Java int array to
an ACL2 list of signed 32-bit integers.
- Char-array-to-ubyte16-list
- Convert a Java char array to
an ACL2 list of unsigned 16-bit integers.
- Boolean-array-to-boolean-list
- Convert a Java boolean array to
an ACL2 list of booleans.
- Double-array-write
- Write a component to a Java double array.
- Boolean-array-write
- Write a component to a Java boolean array.
- Short-array-write
- Write a component to a Java short array.
- Short-array-from-sbyte16-list
- Convert an ACL2 list of signed 16-bit integers to a Java boolean array.
- Long-array-write
- Write a component to a Java long array.
- Int-array-write
- Write a component to a Java int array.
- Float-array-write
- Write a component to a Java float array.
- Char-array-write
- Write a component to a Java char array.
- Char-array-from-ubyte16-list
- Convert an ACL2 list of unsigned 16-bit integers to a Java boolean array.
- Byte-array-write
- Write a component to a Java byte array.
- Byte-array-from-sbyte8-list
- Convert an ACL2 list of signed 8-bit integers to a Java boolean array.
- Boolean-array-from-boolean-list
- Convert an ACL2 list of booleans to a Java boolean array.
- Long-array-from-sbyte64-list
- Convert an ACL2 list of signed 64-bit integers to a Java boolean array.
- Int-array-from-sbyte32-list
- Convert an ACL2 list of signed 32-bit integers to a Java boolean array.
- Short-array-new-init
- Construct a Java short array
with the given initializer (i.e. components).
- Double-array-index-in-range-p
- Check if a Java int is a valid index
(i.e. in range) for a double array.
- Byte-array-new-init
- Construct a Java byte array
with the given initializer (i.e. components).
- Boolean-array-new-init
- Construct a Java boolean array
with the given initializer (i.e. components).
- Boolean-array-index-in-range-p
- Check if a Java int is a valid index
(i.e. in range) for a boolean array.
- Short-array-new-len
- Construct a Java short array
with the given length
and with default components.
- Short-array-index-in-range-p
- Check if a Java int is a valid index
(i.e. in range) for a short array.
- Long-array-new-len
- Construct a Java long array
with the given length
and with default components.
- Long-array-new-init
- Construct a Java long array
with the given initializer (i.e. components).
- Long-array-index-in-range-p
- Check if a Java int is a valid index
(i.e. in range) for a long array.
- Int-array-new-init
- Construct a Java int array
with the given initializer (i.e. components).
- Int-array-index-in-range-p
- Check if a Java int is a valid index
(i.e. in range) for a int array.
- Float-array-new-len
- Construct a Java float array
with the given length
and with default components.
- Float-array-index-in-range-p
- Check if a Java int is a valid index
(i.e. in range) for a float array.
- Double-array-new-len
- Construct a Java double array
with the given length
and with default components.
- Char-array-new-len
- Construct a Java char array
with the given length
and with default components.
- Char-array-new-init
- Construct a Java char array
with the given initializer (i.e. components).
- Char-array-index-in-range-p
- Check if a Java int is a valid index
(i.e. in range) for a char array.
- Byte-array-new-len
- Construct a Java byte array
with the given length
and with default components.
- Byte-array-index-in-range-p
- Check if a Java int is a valid index
(i.e. in range) for a byte array.
- Boolean-array-new-len
- Construct a Java boolean array
with the given length
and with default components.
- Short-array-read
- Read a component from a Java short array.
- Long-array-read
- Read a component from a Java long array.
- Int-array-new-len
- Construct a Java int array
with the given length
and with default components.
- Float-array-read
- Read a component from a Java float array.
- Float-array-new-init
- Construct a Java float array
with the given initializer (i.e. components).
- Double-array-read
- Read a component from a Java double array.
- Double-array-new-init
- Construct a Java double array
with the given initializer (i.e. components).
- Char-array-read
- Read a component from a Java char array.
- Byte-array-read
- Read a component from a Java byte array.
- Boolean-array-read
- Read a component from a Java boolean array.
- Int-array-read
- Read a component from a Java int array.
- Short-array-length
- Obtain the length of a Java short array.
- Float-array-length
- Obtain the length of a Java float array.
- Double-array-length
- Obtain the length of a Java double array.
- Boolean-array-length
- Obtain the length of a Java boolean array.
- Long-array-length
- Obtain the length of a Java long array.
- Int-array-length
- Obtain the length of a Java int array.
- Char-array-length
- Obtain the length of a Java char array.
- Byte-array-length
- Obtain the length of a Java byte array.
