Paper Info
Title
A Formal Framework for Java Separate Compilation
Abstract
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.
Year
Venue
Keywords
2002
ECOOP
java separate compilation,safe compilation schema,compilation schema,formal framework,minimal set,java compilation,sdk implementation,simple corresponding binary language,binary fragment,small java subset,corresponding binary code,operational semantics,type safety
Field
DocType
Volume
Programming language,Dynamic compilation,Java annotation,Computer science,Java concurrency,Real time Java,Theoretical computer science,Generics in Java,Java Modeling Language,Just-in-time compilation,Java
Conference
2374
ISSN
ISBN
Citations 
0302-9743
3-540-43759-2
11
PageRank 
References 
Authors
0.93
12
3
Name
Order
Citations
PageRank
Davide Ancona172769.43
Giovanni Lagorio221217.98
Elena Zucca3497101.25