Skip to content


Switch branches/tags

Latest commit


Git stats


Failed to load latest commit information.
Latest commit message
Commit time

For User: Installation, Compile, Run and Test

In order to use Java Semantics you need the following prerequisites:

Installation process:

$ cd ~
$ git clone --depth=1
$ chmod +x java-semantics/tools/*
$ export PATH=$PATH:~/java-semantics/tools

Before executing programs, you need to compile java-semantics first:

$ cd java-semantics/src

Now you can execute programs bundled with the semantics:

$ ../tests/01_smoke_tests/

Now you can test the execution of multiple programs at once using bundled tool kjtest.

$ --t1 ../tests/01_smoke_tests/

This tool executes each program in the given directory with both Java Semantics and JDK and compares the results. Testing result is summarized in test-results.xml.

For Developer: Kompile and Krun

Instead of using and, developers want to interact with kompile and krun directly.


$ cd java-semantics/src
$ kompile -v --debug -d exec exec/java-exec.k 
$ kompile -v --debug -d prep prep/java-prep.k

Krun: To debug prep semantics:

$ krun --directory "/home/java-semantics/src/prep" --parser "" --symbolic-execution ../tests/01_smoke_tests/

To debug exec semantics (once you have correct pkast file):

$ krun --directory "/home/java-semantics/src/exec" -cMainClass="ListItem(\"helloWorld\")" -cDissolveAllExceptOut="true" --parser "cat" --symbolic-execution

Other docs

Directory docs contains two technical reports: the complete documented semantics of module METHOD_INVOKE and the documentation of the main rule for new instance creation with all the prerequisites.

POPL 15' : K-Java: A Complete Semantics of Java