JIR

JML Intermediate Representation (JIR)

The JML Intermediate Representation offers a means of:

• Decoupling JML tooling back-ends (which are active subjects of research), from JML tooling front-ends (which are a lot of work to develop and maintain and unrelated to verification research).
• Embedding JML specifications into class files using standard Java language features.

JIR related papers include:

• Patrice Chalin, Robby, P. R. James, J. Lee, and G. Karabotsos, “Towards an Industrial Grade IVE for Java and Next Generation Research Platform for JML” , Int. J. on Software Tools for Technology Transfer (STTT), 12(6): 429-446, 2010 (Preprint last updated: January, 2010). Springer page.
• Robby and P. Chalin, “Preliminary Design of a Unified JML Representation and Software Infrastructure”. Proceedings of the 11th Workshop on Formal Techniques for Java-like Programs (FTfJP'09), Genova, Italy, July, 2009.

Tools currently supporting JIR:

• [OpenJir].
  • A tutorial on using OpenJIR.
• [JmlEclipse].

Backends currently making use of JIR:

• Sireum/Kiasan for Java, Robby (SAnToS).