Reference-types
Java reference types [JLS14:4.3].
We formalize Java reference types as syntactic entities.
Reference values are formalized here.
The relevant grammar rules are
the ones in [JLS14:4.3] (for reference-type etc.)
and the ones in [JLS14:4.5.1] (for type-arguments etc.).
The rules in [JLS14:4.3] include annotations,
but the grammar also includes rules for unannotated reference types
in [JLS14:8.3] (for unann-reference-type etc.).
Note, however, that also the rules for unann-reference-type etc.
include some annotations in certain places.
As done in the formalization of primitive types, in our formalization of reference types it seems more practical
to define the `reference types' as the ones without annotations
(not even the ones in the rules for unann-reference-type etc.,
and have a separate notion for `annotated reference types'.
This is just nomenclature, the substance does not change.
For now we just define (unannotated) reference types.
Annotated reference types will be added later.
Subtopics
- Reference-types-definition
- Fixtypes of Java (unannotated) reference types
and mutually recursive companions.
