|
|
|---|
|
|
|
|---|
Java pointers [JLS14:4.3.1].
We formalize pointers to Java objects as opaque entities. Recall that there is no pointer arithmetic in Java.
We model an infinite supply of pointers, i.e. the ability to obtain a new pointer that is distinct from any given finite collection of pointers.
This does not necessarily mean that we model infinite memory, i.e. that it is always possible to allocate new objects. Finite-memory constraints can be captured separately, but in the absence of those constraints, we want the ability to model infinite memory (which is adequate for many purposes, and what all or most existing formalizations do).
The opacity of our pointers does not mean that we cannot model the fact that some Java implementations return an object's pointer (address) as default hash code. We can (optionally) model these hash codes separately from the pointers formalized here: we use these pointers just to identify objects, consistently with [JLS14].
We could use natural numbers to model Java pointers, but we prefer this more abstract model, because it avoids any ``accidental'' properties of pointers entailed by the natural numbers (e.g. one pointer being greater than another one).