Java Type Soundness Revisited

Abstract

We present an operational semantics, type system, and a proof of type soundness for a substantial subset of Java. The subset includes interfaces, classes, inheritance, field hiding, method overloading and overriding, arrays with associated dynamic checks, and exception handling. We distinguish between normal execution, where no exception is thrown - or, more precisely, any exception thrown is handled - and abnormal execution, where an exception is thrown and not handled. The type system distinguishes normal types which describe the possible outcomes of normal execution, and abnormal types which describe the possible outcomes of abnormal execution. The type of a term consists of its normal type and its abnormal type. With this set-up we prove subject reduction. Thus, the meaning of our subject reduction theorem is stronger than usual: it guarantees that normal execution returns a value of a type compatible with the normal type of the term, and that normal execution throws an exception compatible with the abnormal type of the term. We also give a formalization of separate compilation and linking. We distinguish between Javas, Javab and Javar, which stand for the source language, the binary language and the run-time language. Javas closely reflects the Java syntax. Javab is a version of Java where field access and method call are enriched with type information; we consider Javab a high-level version of the byte code. Javar is an extension of Javab where we allow for addresses. Compilation maps Javas onto Javab and uses type information from Javab for the imported classes. The linker checks are reflected as well-formedness checks for Javab. Finally, we show that Javas and Javab can be viewed as a fragment system - an abstract model of separate compilation and linking which was introduced to investigate possible meanings of binary compatibility.