A fully-formalized and extensible minimal imperative fragment of Java.

Java has no module system. Its packages only subdivide the class namespace, allowing only a very limited form of component-level information hiding. A Java Community Process has started designing the Java Module System, a module system for Java 7, the next version of Java. The extensive draft of the design is written only in natural language documents, which inevitably contain many ambiguities.

We design and formalise LJAM, a core of the module system. Where the informal documents are complete, we follow them closely; elsewhere, we make reasonable choices. We define the syntax, the type system, and the operational semantics of this core, defining these rigorously in the Isabelle/HOL automated proof assistant. We highlight the underlying design decisions, and discuss several alternatives and their benefits.

Through analysis of our formalisation, we identify two major deficiencies of the module system: (a) its class resolution is unintuitive, insufficiently expressive, and fragile against incremental interface evolution; and (b) only a single instance of each module is permitted, which forces sharing of data and types, and so makes it difficult to reason about module invariants. We propose modest changes to the module language, and to the semantics of the class resolution, which together allow the module system to handle more scenarios in a clean and predictable manner. To develop confidence, both theoretical and practical, in our proposals, we (a) formalise in Ott the improved module system, iJAM, (b) prove in Isabelle/HOL mechanised type soundness results, and (c) give a proof-of-concept implementation in Java that closely follows the formalisation.

Both of the formalisations, LJAM and iJAM, are based on Lightweight Java (LJ), our minimal imperative fragment of Java. LJ has been a good base language, allowing a high reuse of the definitions and proof scripts, which made it possible to carry out this development relatively quickly, on the timescale of the language evolution process.

Finally, we develop a module system for Thorn, an emerging, Java-like language aimed at distributed environments. We find that local aliasing and module-prefixed type references remove the need for boundary renaming, and that in the presence of multiple module instances, care is required to avoid ambiguities at de-serialisation.

We conclude with a high-level overview of the interactions between the desired properties and the language features considered, and discuss possible future directions.

The proposed Java Module System (JAM) has two major deficiencies, as noted in our previous work: (a) its unintuitive class resolution can often give unexpected results; and (b) only a single instance of each module is permitted, which forces sharing of data and types, and so makes it difficult to reason about module invariants. Since JAM will be a part of Java 7, solving these problems before its release would benefit the majority of Java developers and users. In this paper, we propose modest changes to the module language, and to the semantics of the class resolution, which together allow the module system to handle more scenarios in a clean and predictable manner. To develop confidence, both theoretical and practical, in our proposals, we: (a) formalise the improved module system, iJAM; (b) prove mechanized type soundness results; and, (c) give a proof-of-concept implementation that closely follows the formalisation; these are in Ott, Isabelle/HOL, and Java, respectively. The formalisation is itself modular: iJAM is based on our previous formalization of JAM (LJAM), which extends Lightweight Java (LJ). LJ has shown to be a good base language, allowing a high reuse of the definitions and proof scripts, which made it possible to carry out this development relatively quickly, on the timescale of the language evolution process.