Towards an abstract model of Java dynamic linking and verification

Sophia Drossopoulou

To appear at ACM SIGPLAN Workshop on Types in Compilation (TIC00), Montreal, Canada, 21 September 2000


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.

Server START Conference Manager
Update Time 27 Jul 2000 at 15:10:32
Start Conference Manager
Conference Systems