Precise Type Inference for Java

Welcome to a simple demonstration of our precise constraint-based type inference system for Java ! The system statically checks the type-safety of the downcasts in the analyzed Java program. For theory and algorithms behind the system, please check the project's webpage.

Usage

To test drive our system, submit a Java source file and see the analysis result: safe downcasts will be marked green and unsafe ones will be marked red.

Currently only a single java source file can be submitted. To test with multiple java source files, merge those files into a single file. Please remove all "package the_package_name;" declarations in the file to be submitted.

The system assumes the existence of all java library source code reachable from the analyzed program. We manually convert SUN JDK java library source code to handle native methods and reflections. Currently the system only supports limited java libraries. Please restrict your example to only use libraries java.lang, java.util, and java.io.

To report sever failure or other problems, please contact wtj@cs.jhu.edu.

Examples

Analysis Result of OOPSLA95.java is here. This example is adapted from an example in J. Eifrig, S. Smith, V. Trifonov, Sound Polymorphic Type Inference for Objects, OOPSLA 1995, pp. 169-184.

Analysis Result of BinaryMethod.java is here. This example is adapted from an example in Kim B. Bruce, Luca Cardelli, Giuseppe Castagna, The Hopkins Objects Group, Gary T. Leavens, and Benjamin Pierce. On Binary Methods, Theory and Practice of Object Systems 1 (3), 1995, pp. 217-238.

Analysis Result of HashMap.java is here.

Analysis Result of JLex.java is here. JLex is a Lexical Analyzer Generator for Java.

Analysis Result of Dynamic.java is here. This example shows typical cases of the fundamentally dynamic downcasts.