- Rok Strniša
- Research
- improved Java Module System

# improved Java Module System

improved Java Module System (iJAM) is an extension of Lightweight Java Module
System that gives a more expressive &
intuitive semantics.

## Description

iJAM solves the following two deficiencies with the proposed Java Module System (and formalised within LJAM) that we have identified:

- Unintuitive lookup functions for module and class definitions.
- Too restricted initialization of module definitions.

The language is formalized rigorously: using
the Ott tool, we obtain
the typeset rules *and* its formal definition
(in Isabelle/HOL) from the same source
--- its Ott source files.

## Definition

- Fixing the Java Module System, in Theory and in Practice
[pdf]
[bib].
- Definition in Ott 0.20.1
[lj_common.ott, ljam_commoni.ott, ljp_basei.ott, ljm_basei.ott, ljami.ott] (+ README.txt, Makefile, iJAM.tex).
- Grammar, Typing, and Small-Step Operational
Semantics (generated by Ott, re-ordered).
- Definition in Isabelle/HOL 2008 (generated
by Ott).
- Implementation of iJAM
[API].
- Proof of iJAM's progress and well-formedness
preservation in Isabelle/HOL 2008
[iJAM_eq.thy, iJAM_proof.thy].
- A graph of dependencies between lemmas and
theorems (generated
by Isabelle/HOL).

The above software is released under a New BSD
license.