Source Code

Prototype Implementation 

The implementation is written in OCaml. Since the implementation is still a bit hacky, the source code is not yet freely available here...

The TJSA tool is based on fjavac, an OCaml implementation of a complete Java compiler.  The actual compilation phase has been removed, and the type checking phase has been extended to accomodate for the refined string types and effects.

To solve the constraints, the analyzer relies on the Succinct Solver, which is written in SML/NJ.



The file below contains the same examples that are available in the live demo.

Download Examples