Abstract

This thesis presents K-Java, the first complete formal semantics of Java 1.4,
defined in K Framework. The semantics yields an interpreter and a modelchecker
for multithreaded programs. To test the completeness of K-Java, we
developed our own suite of more than 840 tests that exercise every Java 1.4
feature, corner case or feature interaction. The tests were developed alongside
K-Java, following Test Driven Development. In order to maintain clarity
while handling the great size of Java, the semantics was split into two separate
definitions – a static semantics and a dynamic semantics. The output of the
static semantics is a preprocessed Java program, which is passed as input to
the dynamic semantics for execution. The preprocessed program is a valid
Java program, which uses a subset of the features of Java. The test suite and
the static semantics may be regarded as side contributions, they are generic
and ready to be used in other Java-related projects.

BibTeX