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.