We suggest a model for dynamic linking and verification as in
Java. We distinguish five components in a Java implementation:
evaluation, resolution, loading, verification, and preparation
\HYPHENA with their associated checks. We demonstrate how these
five together guarantee type soundness. We concentrate on giving a
comprehensive description of the role of the five components and
their dependencies, rather than a faithful model of each in
isolation.
We take an abstract view, and
base our model on a language nearer to Java source than to
bytecode. We consider the following features of Java: classes,
subclasses, fields and hiding, methods and inheritance, and
interfaces. We chose these features because the corresponding
checks for each for these is guaranteed by different components.
The main difference between current,
and previous, informally distributed versions of this
work is the study of interfaces, and the more faithful
description of the timing of possible loading.
