Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 Lightweight Java Module System (LJAM)
Lightweight Java Module System (LJAM)
A core design and semantic definition of the Java Module
System.
Author
The language was designed and formalized by Rok
Strniša.
Description
LJAM is Lightweight Java (LJ) extended with a module
system based on early drafts for the Java Module System (JAM): it covers
the core parts of
both JSR-277 and
JSR-294. For those
aspects in the scope of the former, we
follow the
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.
A second
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.
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. Previousy, 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
simplified find_cld_in_imports.
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]; and
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
in LJ];
modules cannot directly import the core module (core_m) any
more;
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
definition);
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
definitions;
added a possible 'bottom' result to find_cld_in_imports_rec; and
minor bug fixes.
Extensions
improved JAM (iJAM): an extension of LJAM that
gives a more expressive & intuitive semantics.