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 (LJ)
Lightweight Java (LJ)
A fully-formalized and extensible minimal imperative
fragment of Java.
Lightweight Java (LJ) is an imperative fragment
of Java. It is intended to be as simple
as possible while still retaining the feel of Java. LJ includes fields,
methods, single inheritance, dynamic method dispatch, and method
overloading. It does not include support for local variables, field hiding,
interfaces, inner classes, or generics.
LJ is largely a simplification of
Middleweight
Java (MJ). A major difference
w.r.t. Featherweight
Java (FJ) is that LJ also models state, whereas FJ is purely
functional. In this sense, LJ is similar
to ClassicJava;
however, unlike ClassicJava, LJ is a proper subset of Java, i.e. every LJ
program is a valid Java program.
LJ 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 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.
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); 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).