Inference of Pluggable Type Systems


A general inference framework for context-sensitive pluggable type systems.


The following instructions assume either a Unix-like (e.g., Linux, Mac).

  1. Download checker-inference.tar.gz. It contains a modified jsr308-langtools, extended Checker Framework and Annotation File Utilities.
  2. Unpack the distribution tar file by running:
      tar xvfz checker-inference.tar.gz
    There are three folders: annotation-tools, checker-framework and jsr308-langtools.
  3. Add the checker-inference/checker-framework/checker/binary directory to your path.
  4. Test Run: Type "javac-ri" in the command line. If you can see
      javac: no source files or class names
      Usage: javac <options> <source files>
      use -help for a list of possible options
    Then the installation is successful.

Using Checker Inference

Infer the immutable references for the Jolden/BH program in the benchmark folder.

          cd checker-inference/checker-framework/checker/
          ./binary/javac-ri benchmark/jolden/bh/*.java

The inference results are dumped to:

Inferring Universe Types and Ownership Types is similar. Just change javac-ri to javac-ut or javac-ot.

Instantiation of other Type Systems

To be done