Java Modeling Language (JML) / News: Recent posts

The jmlspecs CVS repositories are now migrated to CVS control and should no longer be updated from CVS.

A new alpha release of openjml containing an implementation of jmldoc is available from the JML download page. jmldoc combines the javadoc tool of OpenJDK and the JML parsing and checking of the openjml framework in order to create javadoc pages containing JML specifications. It is a drop-in command-line replacement for javadoc.

JML is a design by contract specification language for Java. JML features several tools, including HTML generation, runtime assertion checking, and unit testing. This release includes jmle, a prototype execution tool and also model programs (greybox specifications). There are several other bug fixes and enhancements.

JML is a design by contract specification language for Java. JML features several tools, including HTML generation, runtime assertion checking, and unit testing. This release includes jmle, a prototype execution tool. There are several other bug fixes and enhancements.

JML is a design by contract specification language for Java. JML features several tools, including HTML generation, runtime assertion checking, and unit testing. This release features simplified runtime assertion checking. It still allows JML to be used with a Java 1.5 VM, but not for Java 1.5 sources. There are several other bug fixes and enhancements.

A first (alpha) version of a JML checker for Java 1.6, built from the OpenJDK sources, is now available.

There is now a wiki for JML at
http://jmlspecs.wiki.sourceforge.net/