OTJava is an implementation of Ownership Type System for Java, which I developed as a class project. It works as an Eclpse plugin. The type system is based on David G. Clarke's paper in 1998.
Usage
To use the ownership type system on OTJava, a user must write ownership annotations in the source code. In the current version, annotation must be written using javadoc-style comments. Each annotation should be place right after the type.
Since the original type system doesn't fully cover the entire Java language, neither does this tool. In fact, it doesn't even support inheritance. There are more sophisticated ownership type systems developed by Klarke and other researchers, so it would be desirable that the future version of this tool will use them.
The primitive types (int, double, ...) cannot have context parameters. They can only have an ownership parameter.
Implementation
The implementation depends on the abstract syntax tree provided by the Eclipse JDT (Java Development Tools) library. The library is very useful as it can not only parse the source code and build a syntax tree, but also provide name resolution and type binding. On the other hand, it could consume huge resources especially when analyzing a large program. Therefore, care must be taken to avoid an out-of-memory error.
The current version traverses the ASTs for given source files exactly twice. When the number of files are small, the tool can save all ASTs for all classes. Since this approach requires a lot of memory for a large program,
- In the first path, the tool builds a table of classes which contain an ownership annotation. For each class in the source files to be analyzed, register the ownership types of fields and methods. The classes not analyzed in this step (including library classes) are considered to have no ownership annotation. Each annotation in field and method declarations is checked against
- In the second path, the tool inspects the actual content of the classes for type checking.
[To be updated]