Towards an abstract model of Java dynamic linking and verification
Sophia Drossopoulou · 2007
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 – with their associated checks. We demonstrate how these five together guarantee type soundness. 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.