JML Trac Wiki

The Java Modeling Language (JML) is a behavioral interface specification language that can be used to specify the behavior of Java modules (as in design by contract—DBC). It has many tools to do assertion checking, documentation generation, unit testing, static checking, verification, etc.

Tools

See the JMLSpecs web site for information on downloading various JML tools.

OpenJML

OpenJML is the next generation of the core JML tools and will support Java 1.7. It is based on OpenJDK. We expect our first public release in Summer 2009.

Sub-Projects and Experimental Efforts

• JAJML is an experimental implementation of JML based on JastAdd. 
• JMLTests is a subproject devoted to creating a common testing framework that incorporates the test corpus from JML2 and can be used by the developers of a variety of JML-based tools. 
• JML4 is a (currently suspended) project that investigated a deep embedding of JML tools in the Eclipse JDT
• JML6 is an incomplete, experimental implementation of JML features using Java annotations
• DevelopmentNotes on future directions for JML and JML tool support. 

Legacy Tools

The first publicly available JML tool suite, the Common JML Tools or "JML2", targeted Java 1.4 and earlier.

Documentation

• The JML2 Tool Suite tools are documented using Texinfo and the man file format. A summary of this information is found on the JML2 documentation webpage.
• Information for developers who need to update the documentation can be found on the [JmlDocumentation] page.

Examples

• The JML2 Tool Suite comes with a large collection of example JML-annotated programs.

Semantics

• Discussions about JML's Semantics are summarized on the Wiki, but largely carried out on the jmlspecs-interest mailing list.

Specifications

• JML2 Javadoc API
• OpenJml Javadoc API
• A Beginner's Guide to Specification Writing
• Specification Writing MobiusPve? workspace

Teaching Materials

JML is used in a variety of courses, from early undergraduate through post-graduate, and in industrial and research tutorials. Several people have also developed screencasts and other online resources on formal methods techniques using JML. We’ve begun collecting these materials and links to other resources on our Teaching Materials page.

Credit

• Those responsible for JML.

---

Trac and other links

• TracGuide, WikiFormatting, TitleIndex.
• The Trac project, Trac FAQ, TracSupport.