Overview

• About
• People
• Related Projects
• Download
• Sourceforge

Documentation

• Installation Notes
• ESC/Java2 Plugin
• Project Notes

Support

• Forums
• Bugs/Feature Requests
• Mailing Lists

JMLEclipse is an Eclipse plugin that allows the integration of JML into Eclipse's Java Developmnet Tools (JDT). JMLEclipse is coordinated by the SAnToS Laboratory. At SAnToS we have strong interests in JML mainly due to our work in SpEx.

The whole idea behind JMLEclipse is to have an open framework that can be used as frontend for different JML tools. These frontend provides well-formedness checking and syntax highlighting aid, and other tools can connect as backends, using an open interface, to provide further analysis of JML annotated programs. This situation is depicted in the picture below.

In the current stage, JMLEclipse supports syntax highlighting, type checking and is already interfaced with JML's runtime assertion checker (jmlrac). There is current work to interface SpEx-JML and ESC/Java 2.