JML Editing¶

JML Editing extends the Java development tools (JDT) with support for JML to make writing JML specifications as convenient as writing Java source code.

The following screenshot shows for instance the extended syntax highlighting of the Java Editor:\ JML Editing

Prerequisites¶

JML Editing is compatible with Eclipse Luna (4.4) or newer.

Required update-sites and installation instructions are available in the download area.

Current Functionality¶

Syntax highlighting for JML specifications with configurable colors
Auto completion for JML keywords
Auto indentation of JML comments while writing
Code formatter preserves JML comments
Hovers for JML keywords
Support of JDT\'s Rename and Move Refactorings
Error marker for syntax violations
Profiles for different JML dialects
- Predefined profiles for JML standard and KeY
- Profiles are customizable (by the user)
- Additional profiles can be offered by developers via an Eclipse extension point
- Profiles are based on extendable and configurable JML parsers

Future Work¶

Support for missing JML features
Auto completion within JML keyword content
Specifications shown in the Outline view
Refactorings of JML specifications
Links within JML specifications
Error marker for semantic failures
No spell checking of JML keywords