JTEST

jtest − generate and compile test classes for JML-JUnit testing

jtest [--quiet] [--{make|javac}] file1.java [file2.java] ...

jtest allows a Java(TM) class annotated with JML specifications be tested by using the JUnit unit testing framework. In addition to instrumenting and compiling a Java class for runtime assertion checking (see jmlc(1)), it also generates and compiles separate test oracle and test data classes (see jmlunit(1)). The JML runtime assertions, as compiled by jmlc, are used to decide whether the JUnit tests, generated by jmlunit, succeed or fail. For each Java file, ‘Foo.java’, passed to jtest, jmlc is used to produce a class file, ‘Foo.class’, with that checks the pre- and postconditions, invariants, history constraints, etc. in the JML annotations.

Then jmlunit, is used to generate the file ‘Foo_JML_Test.java’ and, if it doesn’t already exist, the file ‘Foo_JML_TestData.java’. The user should fill in test data in the file, ‘Foo_JML_TestData.java’. This script assumes that has already been done. These files are then compiled, with a CLASSPATH that is set appropriately (see jmlunit(1) and jml-junit(1)).

The user must fill in test data in the ‘init_X’ methods in the ‘*_JML_TestData.java’ files generated by running jtest. However, if the test data in these files is filled in for the first time after running jtest, then the user must either recompile the ‘*_JML_TestData.java’ files or re-run jtest to recompile them.

The program supports the options described below. Multiple uses of the same option generally have no effect that is different than a single use of that option.

Each option has both a short form and two long forms. The long forms consists of one or two hyphens and a word. The short form consists of a hyphen and a single letter. In the synopsis below, the long form is separated from the short form by a comma (,), but in actual usage, you would pick one of these forms and not use the comma.

Note that options are case sensitive.

−−quiet, −quiet, -Q

Shuts off all informational messages. The default is produce these messages.

−−javac, −javac

The generated JUnit test oracle and test data files are compiled by using javac (i.e., javac Foo_JML_Test.class Foo_JML_TestData.java). This is the default, but it can be changed by the option −−make.

−−make, −make

The generated JUnit test oracle file and test data files are compiled using make (e.g., make Foo_JML_Test.class Foo_JML_TestData.class).

The JUnit testing framework should be installed for this command work properly.

CLASSPATH This command sets the CLASSPATH to include the pre-existing CLASSPATH followed by the JUnit jar file, and then JML’s jmlruntime.jar and jmljunitruntime.jar and jmlmodels.jar.

If you get CLASSPATH errors, make sure that ’.’ is in your CLASSPATH variable.

The DOS/Windows batch file version of this command compiles all files named *_JML_Test_*.java that it can find. This will cause compile errors if a file ‘X_JML_TestData.java’ exists but the corresponding ‘X_JML_Test.java’ file does not exist.

With the DOS/Windows batch file, if you have only ’.’ in your CLASSPATH, you will be left with an empty CLASSPATH at the end.

jml(1), jmlc(1), jmlrac(1), java(1), javac(1), junit(1), jmldoc(1), jml-junit(1)

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

Copyright (c) 2001-2003 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.