Practical tools for Java Correctness. We looked at JML, a language for writing assertions in a model-oriented specification style. JML comes with the tools jmlc and jmlunit. We looked at the tool ESC/Java2, which can also use JML annotations. We discussed the common lack of completeness and soundness for tools like this: leading to missed defects and false positives. We mentioned some further and specialised annotations extending core JML (non_null, unreachable, modifies, pure) and specification inheritance. Finally, the FindBugs tool was briefly introduced; it needs no specification at all, but can make use of Java annotations such as @NonNull.
Tips for installing tools
- For JML, try this old release.
- For ESC/Java2, try instructions from earlier this year.
- For FindBugs, visit its downloads page and try out the Eclipse plugin or standalone version.
Please add comments to let us know how you get on!
Posted by David Aspinall 