Lightweight Java (LJ)
A fully-formalized and extensible minimal imperative
fragment of Java.
Authors
The language was designed and formalized by Rok
Strniša and
Matthew Parkinson.
Description
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
overriding. 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.
Documents
The Lightweight Java distributable contains:
An up-to-date Isabelle/HOL proof of
Lightweight Java's progress and well-formedness preservation can now be found at
The Archive of Formal Proofs.
A detailed description of Lightweight Java's design and an overview of its
type soundness proof can be found in the third chapter
of my Ph.D. thesis.
The above documents and software are released under a BSD License.
There is also a Lightweight Java page on Wikipedia.
Development History
- 1th March 2011:
- 5th December 2010:
- Swiched to Ott 0.20.3 and Isabelle2009-2.
- 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
compatible with.
- 4th March 2009:
- Added the judgement for class acyclicity to program
well-formedness.
- 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 `='.
- 16th December 2008:
- Switched to Ott 0.10.15 and Isabelle/HOL 2008.
- 13th 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.
- 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).
- 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).
Extensions
