JML-JUNIT(l)                                                      JML-JUNIT(l)



NAME
       jml-junit  -  run  JUnit  tests  that  were compiled with JML's runtime
       assertion checking compiler

SYNOPSIS
       jml-junit TestDataClassName

DESCRIPTION
       jml-junit runs JUnit tests of a Java(TM) program, named in the TestDat-
       aClassName  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.jml-
       specs.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 CLASS-
       PATH 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 on JUnit's swing  graphical  user  inter-
       face, junit.swingui.TestRunner, 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 JUnit's junit.swingui.TestRunner, which should  be
       consulted for details of its options.

ENVIRONMENT
       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)

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

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: 2003/12/11 17:46:08 $             JML-JUNIT(l)