D. Ancona, G. Lagorio, and E. Zucca
A formal framework for Java separate
compilation
In B. Magnusson, editor, ECOOP'02 - European Conference on
Object-Oriented Programming, volume 2374 of Lecture Notes in Computer
Science, pages 609-635 Springer, 2002
We define a formal notion, called compilation
schema, suitable for specifying different possibilities for
performing the overall process of Java compilation, which
includes typechecking of source fragments with generation of
corresponding binary code, typechecking of binary fragments,
extraction of type information from fragments and definition of
dependencies among them. We consider three compilation schemata
of interest for Java, that is, minimal, SDK and
safe, which correspond to a minimal set of checks, the
checks performed by the SDK implementation, and all the checks
needed to prevent run-time linkage errors, respectively. In
order to demonstrate our approach, we define a kernel model for
Java separate compilation and execution, consisting in a small
Java subset, and a simple corresponding binary language for
which we provide an operational semantics including run-time
verification. We define a safe compilation schema for this
language and formally prove type safety.
[ bib |
.pdf ]
Back
This file has been generated by
bibtex2html 1.43