JMLRAC(l) JMLRAC(l) NAME jmlrac - run Java programs compiled with the JML runtime assertion checker compiler SYNOPSIS jmlrac [--nocheckmodels] [java-option] ... FQClassName DESCRIPTION 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.jml- specs.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.jml- specs.models are provided by adding to the end of the CLASSPATH envi- ronment 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. OPTIONS --nocheckmodels When this option is present, the JML models used are those in the jar file JML/bin/jmlmodelsnonrac.jar, which does not do run- time assertion checking in the org.jmlspecs.models and org.jml- specs.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. EXAMPLES Suppose that the files `PersonMain.java' and `Person.java' have been compiled using jmlc(1). Suppose furhter that both of these files con- tain the package statement package org.jmlspecs.samples.jmltutorial; and hence that they are in the org.jmlspecs.samples.jmltutorial pack- age. Then, assuming that the CLASSPATH environment variable includes the directory just above the directory `org', one can run the `Person- Main' 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 graphi- cal output from your junit tests, you can use jmlrac to run such tests. ENVIRONMENT 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 installa- tion'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. SEE ALSO jmlc(1), java(1), javadoc(1), jml(1), jmldoc(1), jmlunit(1), jtest(1), jml-junit(1) COPYRIGHT 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 FIT- NESS 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. 4th Berkeley Distribution$Date: 2005/08/24 20:41:51 $ JMLRAC(l)