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.
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).