JmlEclipse

[TOC]

JML Eclipse

[JmlEclipse] is an Eclipse-based Integrated Verification Environment (IVE) for Java 6. It uses the Java Modeling Language (JML) as a specification notation and it currently supports:

• Runtime Assertion Checking (RAC).
• Extended Static Checker (pre-alpha).
• Full Static Program Verification (pre-alpha).
• Static Verification via Symbolic Execution.
• Test case generation, including the graphical representation of complex heap structures.

The former is achieved by JML4c, the [JML4]-based RAC tool by Amritam Sarcar and Yoonsik Cheon. The latter two features are offered by Sireum/Kiasan for Java by Robby and other members of the SAnToS team at Kansas State University (KSU).

[JmlEclipse] development is being led by Patrice Chalin (DSRG.org), joined by Robby (SAnToS). For those of you how know a bit about the history of JML tools, [JmlEclipse] is the successor of [JML4] (well, actually, successor of the various JML_n_ projects). It runs under Eclipse 3.5.2, reads JML specifications in the [JML2] input syntax and emits classes files with JML embedded in the JML Intermediate Representation ([JIR]) format. For those of you who recall, this is actually a rebirth of the old SAnToS [JmlEclipse] plug-in. The main paper on [JmlEclipse] is:

• 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.

Also see:

• JML4c: A New Eclipse-Based JML Compiler Built Using AST Merging, Amritam Sarcar and Yoonsik Cheon. TR-10-08 March 2010.
  • Subversion: http://opuntia.cs.utep.edu/svn/repos/jml4/trunk/.
• JML Intermediate Representation ([JIR]).
• OpenJIR.

Using [JmlEclipse]

• A first official (non-beta) release of [JmlEclipse] is targeted for TBD - until we get more developer resources, we might stay in beta for a while [Chalin - 2010/11].
• Our current release roadmap: [JmlEclipse] release for ...
  • Eclipse 3.6: alpha, beta, official.
  • Eclipse 3.7 or e4: no plans yet.
• Download and configuration instructions.

JDT Relevant information

• Eclipse.org page on Extending JDT for Java like languages.
• Bug 186342 - [compiler][null]Using annotations for null checking.

[JmlEclipse] Developer Notes

Note that in some cases a reference is given to a corresponding [JML4] page when the information it contains is still relevant.

Process

• How to contribute to development of the JmlEclipse JDT core (workflow).

How to …

• Setup Eclipse for [JmlEclipse] and run tests to verify installation.
• Build the parser.
• Commit an Eclipse.org "vendor" release.
• Merge the changes of a vendor release into the JML4 JDT Core.
• Launch [JmlEclipse]: Select menu Run >> Run Configurations ... . In the dialog that opens, under Eclipse Applications, choose "[JmlEclipse] (JML4)", then hit the Run button.
• Export: [JmlEclipse] as a plug-in and jml-runtime.jar.

Notes and information

• Developer Journal.
• Architecture and Detailed Design.
• JmlEclipse KSU Jazz Repository.

Older [JML4] notes that may still be relevant:

• JML4 Repository
• JDT, Jikes parser notes
• JML4 Grammar
• Developer Questions and Concerns -- A place for questions and concerns about the JDT architecture.
• Other: TO DO Matrix, Winter School?.