JML-JUNIT

jml-junit − run JUnit tests that were compiled with JML’s runtime assertion checking compiler

jml-junit TestDataClassName

jml-junit runs JUnit tests of a Java(TM) program, named in the TestDataClassName argument, that has been compiled using the JML runtime assertion checker compiler jmlc. It provides the program access to classes in the org.jmlspecs.jmlunit org.jmlspecs.models, and org.jmlspecs.jmlrac.runtime packages. It also provides access to runtime assertion checked version of interfaces in the J2SDK libraries (e.g., in java.lang and java.util). Access to classes in org.jmlspecs.jmlunit and org.jmlspecs.models are provided by adding to the end of the CLASSPATH environment variable the files JML/bin/jmljunitruntime.jar and JML/bin/jmlmodels.jar. Access to the other classes is done by using the Xbootclasspath option of the java program, and using that option to add JML/bin/jmlruntime.jar to the boot class path. With this option set, it runs the java program on JUnit’s swing graphical user interface, junit.swingui.TestRunner, passing along the rest of the aguments.

−−nocheckmodels

When this option is present, the JML models used are those in the jar file JML/bin/jmlmodelsnonrac.jar, which does not do runtime assertion checking in the org.jmlspecs.models and org.jmlspecs.models.resolve packages. The default is to use the models in JML/bin/jmlmodels.jar, which does do runtime assertion of these types.

Aside from the −−nocheckmodels option, this script simply passes along all its arguments to JUnit’s junit.swingui.TestRunner, which should be consulted for details of its options.

The CLASSPATH environment variable is changed by placing the JUnit jar file (‘junit.jar’), the JML/bin/jmljunitruntime.jar, and JML/bin/jmlmodels.jar files at the end of the CLASSPATH during the run. The JML/bin/jmlruntime.jar file is added to the bootclass path.

In the Unix version of this script, the location of the JML installation’s top directory is taken from the JMLDIR environment variable, if that is defined. Similarly, the location of JUnit’s top directory is taken from the JUNITDIR environment variable, if that is defined.

jmlc(1), java(1), javadoc(1), jml(1), jmldoc(1), jmlunit(1), jtest(1)

See the JUnit Web page, http://www.junit.org/, to obtain and install JUnit.

Copyright (c) 2001-2002 by Iowa State University

JML is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 2, or (at your option) any later version.

JML is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details.

You should have received a copy of the GNU General Public License along with JML; see the file COPYING. If not, write to the Free Software Foundation, 675 Mass Ave, Cambridge, MA 02139, USA.