[Prev][Next][Index][Thread]
paper: Towards an abstract model of Java dynamic linking and
The following paper:
Towards an abstract model of Java dynamic linking and
verification
-- version 2 --
Sophia Drossopoulou
and be obtained from
http://www-dse.doc.ic.ac.uk/projects/slurp/pubs.html#dynlink
Abstract
----------
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 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 multiple loaders.
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 different components.
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.
Looking forward to any comments,
Sophia
--
Sophia Drossopoulou http://www-dse.doc.ic.ac.uk/~scd/
Department of Computing,
Imperial College of Science, Technology and Medicine
LONDON SW7 2BZ, England
tel: +44 020 7594 8368, fax: +44 020 7581 8024