Primitive-types
Java primitive types [JLS14:4.2].
We formalize Java primitive types as syntactic entities.
Primitive values are formalized here.
According to the grammar rule for primitive-type [JLS14:4.2],
primitive types (as syntactic entities) include annotations.
The grammar also includes a rule for unann-primitive-type [JLS14:8.3],
which captures the ``core'' eight primitive types without annotations,
as they were in the pre-annotations versions of Java.
However, note that the rules for
integral-type, floating-point-type, and numeric-type
do not include annotations,
even though integral, floating-point, and numeric types
are considered a subset of the primitive types.
For our formalization,
it seems more practical to define the `primitive types'
as the ones without annotations,
and have a separate notion for `annotated primitive types'.
This is just nomenclature, the substance does not change.
For now we just define (unannotated) primitive types.
Annotated primitive types will be added later.
We also formalize the subtype relation on primitive types [JLS14:4.10].
Subtopics
- Primitive-type
- Fixtype of Java (unannotated) primitive types [JLS14:4.2] [JLS14:8.3].
- Primitive-type-<=
- Subtype relation over primitive types [JLS14:4.10].
- Numeric-type
- Fixtype of Java numeric types [JLS14:4.2].
- Primitive-type-<
- Proper subtype relation over primitive types [JLS14:4.10].
- Integral-type
- Fixtype of Java integral types [JLS14:4.2].
- Primitive-type-<1
- Direct subtype relation over primitive types [JLS14:4.10.1].
- Floating-point-type
- Fixtype of Java floating-point types [JLS14:4.2].
