We suggest a model for dynamic linking and verification as in Java.
distinguish five components in a Java implementation: evaluation,
resolution, loading, verification, and preparation - 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, and do not yet consider
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, overloading and
inheritance, interfaces and subinterfaces. We chose these features
because the corresponding checks for each for these is guaranteed by
The main difference between the 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.