The CoJava Tool
©2008 Eric Kerfoot <eric.kerfoot[at]comlab.ox.ac.uk>, licensed under the GPLv2
The CoJava Tool is a research development used in exploration of ownership and concurrency types in Java. The tool accepts
input source of the Java subset language CoJava and produces standard Java output with JML annotations.
This code is then compiled with javac or jmlc. The purpose of the tool is to translate non-JML
annotations used with CoJava to specify unique properties of the language into JML-compliant annotations, and to generate code
for CoJava's concurrency model.
CoJava is a subset of Java using a subset of JML for specification with additional custom annotations. The tool performs
typechecking to enforce the rules required for these custom constructs, and generates code needed for runtime implementation.
The custom annotations and features include:
- Ownership annotations for object types, used to implement a simple method of object ownership. The annotation /*@ owned @*/
is applied to types and the typechecker is used to enforce the custom type rules.
- Colleagues Technique of ensuring the soundness of invariants reliant on externally aliased objects. A colleague annotation
is applied to certain attributes that an invariant may be predicated upon, the typechecker enforces the needed rules and the
code generator creates new JML invariants in the output code.
- Caller contracts introduces the \caller value in contracts that can be used to predicate preconditions on the caller of methods.
The code generator adds an extra Object argument to all generated methods and translates \caller to something JML-compliant.
- Object-based concurrency, a mechanism for encapsulating threads of control as objects is used. This uses the /*@ threaded @*/
annotation applied to types or class definitions that declares objects to be separately-threaded, that is existing in their own thread
of control. Communication with such objects is done using messages that pass non-shared data between threads, ensuring that threads do
not share data and thus are not vulnerable to many classes of concurrency problems. The typechecker enforces needed restrictions on this
mechanism, and the code generator creates the needed proxy classes to enforce the message-passing regime.
This tool is part of my research for a D.Phil in Computer Science at the Oxford University Computing Laboratory.
Download
The CoJava Tool is distributed as a jar file containing compiled code, source code, library definitions, and examples:
Documentation and Examples
- README: The readme file for the jar distribution
- cojava.pdf: CoJava which includes the formal rules for the language
- JavaDoc: Partial JavaDoc documentation
- cojava_iwaco07.pdf: A short paper on CoJava presented at the IWACO workshop at ECOOP '07
- cojava_iwaco09.pdf: CoJava's active object with ownership approach was presented in this paper at the IWACO workshop at ECOOP '09
- These two files are examples of CoJava concurrency and demonstrate two classical concurrency problems. These are also present in the
distribution jar file:
|