Improved Java Module System (iJAM)
An extension of LJAM that gives a more expressive &
intuitive semantics.
Author
The language was designed, formalized, and implemented by Rok
Strniša.
Description
iJAM is based on Lightweight Java Module System
(LJAM). It solves the following two deficiencies with the Java Module
System (JAM) that we have identified:
- unintuitive lookup functions for module and class definitions; and
- too restricted initialization of module definitions.
Please see the documents below for more details.
iJAM 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.
Documents
- Fixing the Java Module System, in Theory and in Practice
[pdf]
[bib]
- Definition in Ott 0.10.16
[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.
Development History
- 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
compatible with.
- 4th March 2009:
- Accessibility constraints of members of the core library module are
now respected.
- 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
for ty.
- 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.
- 2nd December 2008:
- Changed syntax of boundary renaming
from rename(br, fqn) to br[fqn].
- Corrected the semantics of class resolution. Specifically, now an
import mi is not searched if
br[fqn] ∉ fqns, i.e. if (possibly)
renamed fqn is not exported by mi, OR if fqn
∉ dom(br) ∧ fqn ∈
ran(br), i.e. if "fqn does not have a different name in
mi, AND some (other) name has fqn as a different name in
mi." Only the second part of the condition was added, which states
that boundary renaming is, in fact, renaming, and not aliasing, i.e. the
original name is hidden. Corrected the type soundness proof
accordingly.
- Corrected the implementation so that it: (1) does not support boundary
renaming in the compatibility mode; and, (2) definitely searches the
imports as they are declared in the corresponding module file.
- 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.
- 30th April 2008:
- All the semantics has been updated according to changes
in LJAM.
- The implementation has been updated to use renaming. The accompanying
example has also been updated.
- The proof of type soundness is now available online.
|
|
|