Primitive-values
Java primitive values [JLS14:4.2].
We formalize the Java boolean and integral values.
We also provide abstract notions of the Java floating-point values,
as a placeholder for a more precise formalization of them.
Our formalization tags the Java primitive values
with an indication of their types
(and, for floating-point values, of their value sets),
making values of different types (and of floating-point value sets)
disjoint.
This will allow us
to define a defensive semantics of Java
and to prove that the static checks at compile time
guarantee type safety at run time,
as often done in programming language formalizations.
Subtopics
- Floating-pointx-value
- Fixtype of Java floating-point values [JLS14:4.2.3],
including extended-exponent values [JLS14:4.2.3].
- Doublex-value-fns
- Recognizer, fixer, constructor, and destructor of
Java double values
in the double-extended-exponent value set [JLS.4.2.3].
- Primitivex-value
- Fixtype of Java primitive values [JLS14:4.2],
including extended-exponent values [JLS14:4.2.3].
- Floatx-value-fns
- Recognizer, fixer, constructor, and destructor of
Java float values
in the float-extended-exponent value set [JLS.4.2.3].
- Primitive-value
- Fixtype of Java primitive values [JLS14:4.2],
excluding extended-exponent values [JLS14:4.2.3].
- Numericx-value
- Fixtype of Java numeric values [JLS14:4.2],
including extended-exponent values [JLS14:4.2.3].
- Numeric-value
- Fixtype of Java numeric values [JLS14:4.2],
excluding extended-exponent values [JLS14:4.2.3].
- Integral-value
- Fixtype of Java integral values [JLS14:4.2.1].
- Int-value
- Fixtype of Java int values [JLS14:4.2.1].
- Char-value
- Fixtype of Java char values [JLS14:4.2.1].
- Byte-value
- Fixtype of Java byte values [JLS14:4.2.1].
- Short-value
- Fixtype of Java short values [JLS14:4.2.1].
- Long-value
- Fixtype of Java long values [JLS14:4.2.1].
- Float-value
- Fixtype of Java float values
in the float value set [JLS14:4.2.3].
- Double-value
- Fixtype of Java double values
in the double value set [JLS14:4.2.3].
- Boolean-value
- Fixtype of Java boolean values [JLS14:4.2.5].
- Floating-point-value
- Fixtype of Java floating-point values [JLS14:4.2.3],
excluding extended-exponent values [JLS14:4.2.3].
- Disjoint-primitive-values
- The tagging keywords make all the primitive values disjoint.
- Short-value-list
- Fixtype of lists of Java short values.
- Long-value-list
- Fixtype of lists of Java long values.
- Int-value-list
- Fixtype of lists of Java int values.
- Float-value-list
- Fixtype of lists of Java float values.
- Double-value-list
- Fixtype of lists of Java double values.
- Char-value-list
- Fixtype of lists of Java char values.
- Byte-value-list
- Fixtype of lists of Java byte values.
- Boolean-value-list
- Fixtype of lists of Java boolean values.
