Lightweight Java Module System (LJAM)
A core design and semantic definition of the Java Module
The language was designed and formalized by Rok
LJAM is Lightweight Java (LJ) extended with a module
system based on early drafts for the Java Module System: it covers the core
parts of both JSR-277 and
JSR-294. For those
aspects in the scope of the former, we
informal description closely; for the remainder, we try to capture what
we believe is the intended semantics. At the time of development of LJAM,
JSR-294 only a simple straw-man proposal (which is no longer
straw-man proposal for JSR-294 has been written since. It does not
introduce significant changes to the first one, but rather goes into more
details. LJAM corresponds closely to this one too, except that LJAM does
not have support for inner modules.
LJAM 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.
- The Java Module System: Core Design and Semantic Definition (OOPSLA'07
paper, © ACM, 2007) [pdf]
- Definition in Ott 0.20.1
[lj_common.ott, ljam_common.ott, ljp_base.ott, ljm_base.ott, ljam.ott]
(+ README.txt, Makefile, ljam.tex)
- Grammar, Typing, and Small-Step Operational
Semantics (generated by Ott, re-ordered)
- Definition in Isabelle/HOL 2008 (generated
- Proof of LJAM's progress and well-formedness
preservation in Isabelle/HOL 2008
- A graph of dependencies between lemmas and
The above software is released under a New BSD
- 26th June 2010:
- Swiched to Ott 0.20.1: making use of the new -i and -o options.
- 10th March 2009:
- Switched to Ott 0.10.16: the flag -isabelle_inductive false
was added to Ott's parameters, which forces Ott to generate set-based (not
predicate-based) inductive definitions, which our existing proofs are
- 4th March 2009:
- Accessibility constraints of members of the core library module are
- Well-formed program change (relation used in the type soundness proof)
is now defined in Ott.
- Empty lists now presented with `' in LaTeX output. Empty before.
- Added meta-aliases for a few meta-variables and terms: Field
for f, Method for meth, Pointer for oid,
TVar for x, C for cl, and Type
- Updated descriptions of terms and rule definitions.
- Changed the symbol for meta-equality from `==' to `='.
- 17th December 2008:
- Switched to Ott 0.10.15 and Isabelle/HOL 2008.
- 14th October 2008:
- Improved documentation of the distribution of Ott sources.
- Made it easy to re-compile Ott files through a Makefile.
- Improved LaTeX output.
- 27th May 2008:
- The type of the heap H is: oid ⇀ (τ, f
⇀ v). For a field-value update production
(H[(oid, f) ↦ v]), we first need to look
up the mapping for oid in H. Previously, if such a mapping did
not exist, the Isabelle/HOL semantics was to simply return the original
heap H, ignoring the field-value update production; this was fine,
because the mapping provably exists everywhere we used this
production. However, to remove the need for such proofs, we now updated the
Isabelle semantics so that it instead returns "arbitrary" (a value of any
type about which nothing is known) in the mentioned case. With this
definition, any wrong usage of the production is automatically detected by
the soundness proof (no such wrong usages were found).
- 21th May 2008:
- Made it clearer in the meta-syntax that path_length is a
relation, not a function.
- 8th April 2008:
- Corrected the semantics of and
- 28th March 2008:
- Previously defined in terms of program size, the termination condition
for the relation defining the function for finding class hierarchy paths
(find_path_rec) is now defined in terms of acyclicity property
among class definitions (acyclic_clds) [a change reflected by a
change in LJ].
- ftype_in_path now correctly fails (returns ⊥) when the
type of the field being searched for cannot be found (previously, it
simply skipped such field declarations) [a change reflected by a change
- Modules cannot directly import the core module (core_m) any
- Previously defined in terms of the number of module instances in the
system, the termination condition for the relation defining the function
for finding classes in module imports (was find_cld_in_imports_rec,
now find_cld_in_imports) is now defined in terms of acyclicity
property among module instances (acyclic_mh).
- Administration actions can now only instantiate normal modules (not
also the core_m, which must already be instantiated by
- Type-checking is now the last step when creating a new module instance
(r_new_instance), which made the
type-preservation proof easier.
- 7th February 2008:
- Meta-type distinction between source definitions and type-checked
- Added a possible 'bottom' result to find_cld_in_imports_rec.
- Minor bug fixes.