Quis-Custodiet

Java2Jinja

JinjaThreads is a formal semantics for multithreaded Java and Java bytecode in the proof assistant Isabelle/HOL.

The Eclipse plug-in Java2Jinja converts Java programs into JinjaThreads syntax and provides a front-end for JinjaThreads' interpreter and virtual machine.

System requirements

Java2Jinja requires the following software:

Eclipse (tested with version 3.7.1)
PolyML (tested with version 5.4.1)

Download and installation

Install the Java2Jinja plugin for Eclipse from the update site at
http://pp.ipd.kit.edu/projects/quis-custodiet/Java2Jinja/Java2JinjaUpdateSite
Download a customized standard library for Java (jdk_classes.jar)
Download and unzip the generated ML code for JinjaThreads
Set the path names of the ML files and PolyML on the Java2Jinja preference page in Eclipse (Window/Preferences)
If you want to compile the code and run the JinjaThreads VM instead of the source code interpreter, choose JVM_Execute2.ML instead of J_Execute.ML.
Create a new project and adapt the build path as follows:
- Add jdk_classes.jar to the referenced libraries
- Ensure that it precedes the JRE system library in the build path order.
Test your installation by running Java2Jinja (toolbar buttons between printing and debugging or via the Run menu) on the following HelloWorld program:
```
    class HelloWorld {
      public static void main(String[] args) {
        System.out.println("Hello, world!");
      }
    }
    
```

Development

Java2Jinja is a research prototype. Browse the GIT repository for the latest development.