In order to use Java Semantics you need the following prerequisites:
- Linux.
- Java 8 or later (K Framework installation might require more updated Java version).
- K Framework (See http://kframework.org). The bin directory should be added to PATH. (Currently K is upgrading, please use this version of K https://github.com/kframework/k-legacy/tree/javaCompatible)
Installation process:
$ cd ~
$ git clone --depth=1 https://github.com/kframework/java-semantics.git
$ 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
$ kjkompile.sh
Now you can execute programs bundled with the semantics:
$ kjrun.sh ../tests/01_smoke_tests/helloWorld.java
Now you can test the execution of multiple programs at once using bundled tool kjtest.
$ kjtest.sh --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.
Instead of using kjkompile.sh and krun.sh, developers want to interact with kompile and krun directly.
Kompile:
$ 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 "kj-parse-aggreg.sh" --symbolic-execution ../tests/01_smoke_tests/helloWorld.java
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 helloWorld.java.pkast
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.
http://fsl.cs.illinois.edu/index.php/K-Java:_A_Complete_Semantics_of_Java