JMLRAC

jmlrac − run Java programs compiled with the JML runtime assertion checker compiler

jmlrac [--nocheckmodels] [java-option] ... FQClassName

jmlrac runs a Java(TM) program, named in the FQClassName 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, 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 java, which should be consulted for details of its options.

Suppose that the files ‘PersonMain.java’ and ‘Person.java’ have been compiled using jmlc(1). Suppose furhter that both of these files contain the package statement

package org.jmlspecs.samples.jmltutorial;

and hence that they are in the org.jmlspecs.samples.jmltutorial package. Then, assuming that the CLASSPATH environment variable includes the directory just above the directory ‘org’, one can run the ‘PersonMain’ class as compiled with jmlc as follows.

jmlrac org.jmlspecs.samples.jmltutorial.PersonMain

If you are using the jmlunit(1) tool, you may want to use the jml-junit(1) script instead of jmlrac. However, if you do not want graphical output from your junit tests, you can use jmlrac to run such tests.

During the execution of the program, 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), jml-junit(1)

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.