JMLRE

jmlre − run Java programs compiled with the JML executable specification compiler

jmlre [java-option] ... FQClassName

jmlre runs a Java(TM) program, named in the FQClassName argument, that has been compiled using the JML executable specification compiler jmle. It provides the program access to classes in the org.jmlspecs.jmlexec package by adding to the end of the CLASSPATH environment variable the file JML/bin/jml-release.jar.

This script simply passes along all its arguments to java , which should be consulted for details of its options.

Suppose that the file ‘Test.jml’ has been compiled using jmle(1), and that the file ’TestTest.java’ (which has a main method that creates instances of class Test and uses them to call methods specified in class Test) has been compiled using javac(1). Then one can run the TestTest class as follows.

jmlre TestTest

If class TestTest is located in some package, then the fully qualified package name should be specified in the command line to jmlre .

During the execution of the program, the CLASSPATH environment variable is changed by placing the JML release jar file (‘jml-release.jar’) at the end of the CLASSPATH during the run.

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.

jmle(1), 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.