|
jmlunit − generate file for running JUnit tests on JML annotated Java files |
|
jmlunit [option] ... file-or-directory-or-package [file-or-directory-or-package] ... jmlunit-gui [option] ... file-or-directory-or-package [file-or-directory-or-package] ... |
|
For each Java(TM) or JML source file, and for the top-level class or interface defined in that source file with the name of the source file, the commmand jmlunit, or the graphical user interface version jmlunit-gui , generates code for an abstract test oracle class, that can be used to test that class or interface with JUnit. For example, if jmlunit is given a file ‘Foo.java’, containing a top-level class ‘Foo’, then it generates code for a test oracle class ‘Foo_JML_Test’ and places it in ‘Foo_JML_Test.java’. By default, the tool also generates another file to hold a subclass of the test oracle class, unless that file already exists. For example, if jmlunit is given a file ‘Foo.java’, containing a top-level class ‘Foo’, then if the file ‘Foo_JML_TestData.java’ does not exist, it generates a class ‘Foo_JML_TestData’ and places it in that file. The user is supposed to edit the concrete subclass of ‘Foo_JML_Test’ in ‘Foo_JML_TestData.java’ to provide the test data used in the testing. This behavior can be suppressed by the use of the -t option. The file ‘Foo_JML_TestData.java’ is used to hold test data. Comments in the file indicate how to supply test data. Note that it is safe to add test data to such ‘_JML_TestData.java’ files, because such files are never modified by jmlunit if they exist. When given a directory argument instead of a file argument, jmlunit processes all the ‘.java’ files in that directory that do not have names that end in ‘_JML_Test.java’ or ‘_JML_TestData.java’. The jmlunit script sets the CLASSPATH and then runs the Java class org.jmlspecs.jmlunit.Main, which generates a test oracle class and, if necessary, a test data class for each named Java source file. The jmlunit-gui script is similar, but just runs the Java class org.jmlspecs.jmlunit.JntGUI, which brings up a graphical user-interface to do the work. If jmlunit finds an error, the file name, line number, and column number where the error occurred are reported. In such cases, by default, no output will be produced for the file with the error and the following files. See the EXAMPLES section below for a more tutorial introduction to using jmlunit. |
|
The jmlunit script and the graphical user interface support the options described below. On the command line, one can give the options in the form described below; the graphical user interface has other ways to select files and set the options. Both options without arguments and options with arguments simply set the option as indicated by the description below. Multiple uses of the same option generally have no effect that is different than a single use of that option. For the command line, each option has both a short form and two long forms. The long forms consists of one or two hyphens and a word. To avoid duplication, we only show the long forms with two hyphens, since these are unambiguous; however one can use the forms with a single hyphen if desired. To avoid ambiguity between multiple short form options and the long form with a single hyphen, one should give each option separately. 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 on the command line are case sensitive. |
|
−−testdata, −t |
|
Do not generate Java source code for a skeleton test data class. By default, if this option is not used, for a file ‘Foo.java’, this source code would be put in a file named ‘Foo_JML_TestData.java’. However, an existing file with this name will never be overwritten if it already exists. The test data class inherits from the generated test oracle class, e.g., from the class in ‘Foo_JML_Test.java’. The default is to produce this skeleton test data file. |
|
−−classpath <directory-list>, -C <directory-list> |
|
Use the given string as the CLASSPATH during compilation. By default the value of the environment variable CLASSPATH is used instead. |
|
−−debug, −c |
|
Produces (copious) debugging information. The default is not to produce this information. |
|
−−deprecation, −D |
|
Generate tests for deprecated members in the ‘‘_JML_Test.java’’ file. The default is not to generate tests for such deprecated members. |
|
−−destination <directory>, −d <directory> |
|
Writes files (such as the ‘_JML_Test.java’ file) in a subdirectory corresponding to the file’s package name, relative to the named destination directory. The default is to write such files in the directory in which the source files reside (which may not be the current directory). |
|
−−filter <String>, −f <String> |
|
Make the warning filter be the named class. The default is org.multijava.mjc.DefaultFilter. |
|
−−generic, −G |
|
Accept the Java 1.5 generic syntax. This feature is still experimental. The default is not to do this. |
|
−−help, −h |
|
Display the help information and exit. The default is not to do this. |
|
−−keepGoing, −k |
|
Keep going when errors are encountered. Be warned that this may cause the tool to die with an exception. The default is to not keep going. |
|
−−multijava, −M |
|
Accept MultiJava source code. The default is to not accept Multijava constructs. |
|
−−nomultijava |
|
Do not accept MultiJava source code. This turns off acceptance of Multijava constructs. |
|
−−package |
|
Generate tests for all but private methods and constructors in the named files. The default is to only generate tests for public methods and constructors. This is equivalent to the -L2 option. |
|
−−packageName, −N |
|
The name of the package for the generated classes. The default is the same package as the source files. An empty string argument produces generated classes in the unnamed package. If the argument ends in a ’+’, then the argument is prefixed (with a separating ’.’ character replacing the ’+’) to the package name of the source file. |
|
−−protected |
|
Generate tests for public and protected methods and constructors in the named files. The default is to only generate tests for public methods and constructors. This is equivalent to the -L1 option. |
|
−−public |
|
Generate tests for only the public methods and constructors in the named files. This is the default, and is also equivalent to the -L0 option. |
|
−−quiet, −q |
|
Do not suppress information on compilation passes completed. The default is to suppress this information. |
|
−−recursive, −R |
|
Process all subdirectories of given directory and package arguments recursively. The default is not to process subdirectories. |
|
−−relaxed, −r |
|
Accept Relaxed MultiJava source code. The default is not to allow the special constructs in Relaxed MultiJava. |
|
−−safemath, −s |
|
Turns on safe math mode. This is an experimental feature, currently under development, in which the checker will report a compile-time error if the evaluation of a constant integral expression causes an overflow. The default is not to report such errors. |
|
−−source <release-number> |
|
Accept code containing source for the given Java version. When the release-number is "1.4", the compiler accepts code containing Java 1.4 assert statements, and treats ‘assert’ as a reserved word in Java code. The default is "1.3", meaning that ‘assert’ is not a reserved word in Java code (although it is in annotations). In some future release of JML, the default will change to "1.4". |
|
−−sourcepath <directory-list>, −S <directory-list> |
|
Use the given path when searching for Java and annotation source files. A path is a list of directories separated by either colons (on Unix) or semicolons (on Windows). The default is to use the CLASSPATH. |
|
−−testLevel=<int>, −L<int> |
|
Select, according to their declared access level, the set of methods and constructors to generate test methods for. Possible values are: 0 for public, 1 for public and protected, and 2 for public, protected and package. For example, specifying 0 generates test methods only for public methods and constructors. The default is 0. |
|
−−universes, −e |
|
Enable Universe type modifiers and checking. This feature is not enabled by default. |
|
−−universesx <String>, −E <String> |
|
Specify the degree of support for the Universe type modifiers and checking. The string option can be either "no", "parse", or "full". The option "no", means that these features are not recognized; this is the default. The option "parse", means that these features are parsed but not used otherwise. The option "full", means that these features are checked during type checking. |
|
−−useGenerator, −g |
|
Without this option the ‘_JML_TestData’ file is created with inline comments at those points in the file where the user must added test data generation code. This is a problem when the file being subject to test is changed (because the inlined data generate code must be recopied into any newly generated ‘_JML_TestData’ file. Use of this option will cause the ‘_JML_TestData’ file to make use of calls to a test data generation class instead of requiring inlined code. Hence, even if the file being subject to tests is changed, no inlined code need to be copied; instead simply rerun jmlunit with the -g. IMPORTANT NOTE: use of this option will always generate a ‘_JML_TestData’ file, overwriting one if it exists. By default, the name of the test data generator class is ‘TestDataGenerator’. To change this default use ‘-generatorClassName’ and to change the package (from the default package) use ‘-generatorPackageName’. |
|
−−verbose, −v |
|
Display verbose information during compilation. The default is not to display this information. |
|
−−version, −V |
|
Istead of doing anything else, print the checker’s version information on standard output and exit. The default is not to do this. |
|
−−warning=<int>, −w<int> |
|
Set the ‘pickiness’ of warnings displayed to the given integer. The default is 1. Using 2 generates more picky warnings, and 3 more picky still. |
|
−−Xnoversion |
|
Omits printing the version in help messages, which is useful for regression testing (but not normally by users). The default is to print the version in help messages. |
|
Normal usage |
|
Suppose you have a file ‘Person.java’, containing a class ‘Person’. The first step is to execute |
jmlc Person.java |
|
to compile the code and specifications using JML’s runtime assertion checking compiler. This is helpful in settling the specification of the class. Next, you start using jmlunit. After executing |
jmlunit Person.java |
|
you will then have two files |
Person_JML_Test.java Person_JML_TestData.java |
|
in the current directory. The first file, ‘Person_JML_Test.java’ has methods to test all the methods of class Person, but does not have any test data. |
|
Supplying Test Data |
|
To supply test data, you have to fill in the data in the file ‘Person_JML_TestData.java’. You do this by following the directions written in that file’s comments. These comments will indicate some places to fill in code that supplies test data of each type needed. Contining the ‘Person’ example, suppose that the methods in class Person have arguments of types ‘Person’, ‘int’, and ‘String’. In this case, the file ‘Person_JML_TestData.java’ will contain methods named ‘vpkg_name_PersonIter’ (assuming that Person lives in the package pkg.name), ‘vintIter’, and ‘vjava_lang_StringIter’. These test data supplly methods are called by the test driver when it needs test data of the corresponding type. Usually one can supply appropriate test data without changing the test data supply methods directly, by changing the initialization for the strategy objects that are used in the bodies of these methods. For example, the ‘vpkg_name_PersonIter’ method has the following body |
return vpkg_name_PersonStrategy.iterator(); |
|
which indicates that you can supply test data by changing the initializer for the strategy object named ‘vpkg_name_PersonStrategy’ in the class. Initially, the output of jmlunit would contain an initializer for ‘vpkg_name_PersonStrategy’ that looks as follows (assuming that Person is a class without a public ‘clone’ method). |
/** The strategy for generating test data of type
* pkg.name.Person. */
private org.jmlspecs.jmlunit.strategies.StrategyType
vpkg_name_PersonStrategy
= new org.jmlspecs.jmlunit.strategies.NewObjectAbstractStrategy()
{
protected Object make(int n) {
switch (n) {
// replace this comment with test data if desired
default:
break;
}
throw new java.util.NoSuchElementException();
}
};
|
|
In this case you would replace the comment in the body of the ‘switch’ statement with code to return various Person objects for use in testing. The class ‘NewObjectAbstractStrategy’ (which is being extended in place in this example to override the method ‘make’), supplies ‘null’ as the only test data by default, so one does not need to supply that piece of data explicitly. Instead, one should write code for various more interesting Person objects. For example, the following might be suitable as the edited version of this field’s initialization. |
/** The strategy for generating test data of type
* pkg.name.Person. */
private org.jmlspecs.jmlunit.strategies.StrategyType
vpkg_name_PersonStrategy
= new org.jmlspecs.jmlunit.strategies.NewObjectAbstractStrategy()
{
protected Object make(int n) {
switch (n) {
case 0:
return new Person("Yoonsik");
case 1:
return new Person("Clyde");
case 2:
return new Person("Curt");
default:
break;
}
throw new java.util.NoSuchElementException();
}
};
|
|
To supply test data of type ‘String’ is easier. The method ‘vjava_lang_StringIter’ has the following body. |
return vjava_lang_StringStrategy.iterator(); |
|
Thus to supply the test data, one changes the initializer for the ‘vjava_lang_StringStrategy’. Initially, jmlunit generates the following code for this initializer. |
/** The strategy for generating test data of type
* java.lang.String. */
private org.jmlspecs.jmlunit.strategies.StrategyType
vjava_lang_StringStrategy
= new org.jmlspecs.jmlunit.strategies.StringStrategy()
{
protected java.lang.Object[] addData() {
return new java.lang.String[] {
// replace this comment with test data if desired
};
}
};
|
|
By default the type ‘StringStrategy’ provides only a minimal amount of test data (namely ‘null’ and the empty string). To supply additional test data, one can replace the comment in the array initializer with a list of additional test data. For example, to add the strings "Curt", "Joe", and "Patrice", one would write: |
/** The strategy for generating test data of type
* java.lang.String. */
private org.jmlspecs.jmlunit.strategies.StrategyType
vjava_lang_StringStrategy
= new org.jmlspecs.jmlunit.strategies.StringStrategy()
{
protected java.lang.Object[] addData() {
return new java.lang.String[] {
"Curt", "Joe", "Patrice",
};
}
};
|
|
(The comma at the end of the edited line is not needed, but makes adding more data later easier.) Similarly, to supply test data of type ‘int’ one would change the initializer for the field ‘vintStrategy’. Initially, jmlunit generates an initializer that looks like the following. |
/** The strategy for generating test data of type
* int. */
private org.jmlspecs.jmlunit.strategies.IntStrategyType
vintStrategy
= new org.jmlspecs.jmlunit.strategies.IntStrategy()
{
protected int[] addData() {
return new int[] {
// replace this comment with test data if desired
};
}
};
|
|
By default the type ‘IntStrategy’ provides only a minimal amount of test data (namely -1, 0, and 1). To supply additional test data, one can replace the comment in the array initializer with a list of additional test data, as shown above in the example of supplying test data for strings. An alternative is to use a different strategy. For each primitive Java type, T, JML provides a strategy named TBigStrategy that has more test data. For example, there is a strategy named ‘IntBigStrategy’ (in the package org.jmlspecs.jmlunit.strategies) that supplies more test data of type ‘int’ than does ‘IntStrategy’. (For example, ‘IntBigStrategy’ includes 3, -5, ‘Integer.MIN_VALUE’, and ‘Integer.MAX_VALUE’.) To use ‘IntBigStrategy’ to initialize the field ‘vintStrategy’ one would edit the automatically generated initializer to look as follows. |
/** The strategy for generating test data of type
* int. */
private org.jmlspecs.jmlunit.strategies.IntStrategyType
vintStrategy
= new org.jmlspecs.jmlunit.strategies.IntBigStrategy();
|
|
Documentation for the various strategies is included in the JML release is found in the jmldoc-produced documentation for the org.jmlspecs.jmlunit.strategies package, which is included in the JML release. (Use the file ‘JML.html’, located in the top level directory of the release, to access this and other JML documentation that ships with the release. You have to click on the ‘‘Description’’ link at the top, or scroll down past the lists to see this overview document.) |
|
Dealing with Changes |
|
Note that your edits to the ‘_JML_TestData.java’ file will not be lost when you run jmlunit again, as jmlunit never changes such files if they exist. However, if you add new methods to a class that have types of arguments that were not present the first time you ran jmlunit, then you can do one of two things. One is to put in code for methods that supply test data of the appropriate type by hand, following the pattern used in the file already to write the required code. Another option is to first move the ‘_JML_TestData.java’ file to another file name (but not one ending with ‘_JML_Test.java’!). Then rerun jmlunit to generate a new ‘_JML_TestData.java’ file. Finally, merge in your old test data initializations into the new file, and add initializations to supply test data of the new types. |
|
Running the Tests |
|
After supplying the test data by editing the file ‘Person_JML_TestData.java’ you can compile and run the tests. First, compile the code in the ‘Person_JML_Test.java’ and ‘Person_JML_TestData.java’ files. These can be compiled using a normal java compiler (e.g., mjc or javac); however, you must have the JUnit jar file (‘junit.jar’), and two of JML’s jar files, namely ‘JML/bin/jmlruntime.jar’ and ‘JML/bin/jmljunitruntime.jar’, in your CLASSPATH for this compilation to work, as in the following example (for Linux): |
export CLASSPATH=.:/opt/junit/junit.jar:/opt/JML/bin/jmlruntime.jar:/opt/JML/bin/jmljunitruntime.jar javac Person_JML_Test*.java |
|
If you have all of these in your CLASSPATH, then you can use the java interpreter (i.e., the command java(1)), to run the tests, as in the following example (for Linux): |
java pkg.name.Person_JML_Test |
|
Alternatively one can test this using the command jml-junit(1), which sets the CLASSPATH automatically, as follows, |
jml-junit pkg.name.Person_JML_Test |
|
where ‘pkg.name’ is the name of the package that contains the class ‘Person’, to run JUnit on the result. It is also possible to use a command such as |
jmlrac pkg.name.Person_JML_Test org.jmlspecs.junit.JMLTestRunner |
|
to get JML’s text version of the test runner, which is found in JML/bin/jmljunitruntime.jar. The jmlrac(1) script is like jml-junit, but uses a text-based instead of a graphical user interface. It avoids the need to carefully adjust the CLASSPATH for yourself to include the appropriate jar files (as described above), which you would have to do if you use java directly. |
|
Use of -t |
|
The command |
jmlunit -t Person.java |
|
will generate only the file ‘Person_JML_Test.java’, and will never generate ‘Person_JML_TestData.java’ (even if it does not exist). This is useful if you already have a test data class, or if the test data class has a different name other than ‘Person_JML_TestData’. |
|
The CLASSPATH environment variable is used to find Java class and source files, as well as JML specification files. |
|
The jmlunit script sets the CLASSPATH environment variable, but does not look at any -classpath option that might be used. If you use a -classpath option, then you must explicitly include paths to the jar files and directories that this script would have otherwise included. On the other hand, this allows you to override the default orderings for such jar files and directories. |
|
If you get CLASSPATH errors when compiling the files generated by jmlunit, make sure that, besides the directories you would otherwise need to have in your CLASSPATH, your CLASSPATH environment variable’s value also includes the JUnit jar file (‘junit.jar’), and JML’s ‘jmlruntime.jar’ and ‘jmljunitruntime.jar’. These last two jar files are found in the JML release’s directory, under the bin directory (‘JML/bin’). If you use the classes in the package org.jmlspecs.models, then you will also need to include JML’s jar file ‘jmlmodels.jar’, which is also found under JML’s bin directory ‘JML/bin’. Verify that these are present in your system and that the path names are correct. The script jtest(1) manages these CLASSPATH issues for compilation, and the scripts jmlrac(1) or jml-junit(1) can be used to manage them during the running of the tests. |
|
jtest(1), jmlc(1), jml-junit(1), jmlrac(1), jml(1), java(1), jmldoc(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. |