![[ICO]](/icons/blank.gif){kind=icon}
![[PARENTDIR]](/icons/back.gif){kind=icon}
![[DIR]](/icons/folder.gif){kind=icon}
![[TXT]](/icons/text.gif){kind=icon}
| Name | Last modified | Size | Description |
|---|---|---|---|---|
| Parent Directory | - | ||
| specs/ | 2013-08-08 14:16 | - | |
| org/ | 2009-03-16 14:02 | - | |
| javadocs/ | 2009-03-16 13:22 | - | |
| etc/ | 2009-03-16 14:02 | - | |
| docs/ | 2009-03-16 13:09 | - | |
| bin/ | 2009-03-16 13:21 | - | |
| WARRANTY.txt | 2005-07-07 17:03 | 723 | |
| README.html | 2006-01-18 17:33 | 21K | |
| NEWS.txt | 2009-03-16 10:49 | 3.5K | |
| LesserGPL.txt | 2005-07-07 17:03 | 26K | |
| JML.html | 2008-05-20 18:17 | 17K | |
| COPYING.txt | 2002-03-15 16:43 | 18K | |
This is a release of a set of tools, examples, and documentation for the Java Modeling Language (JML), obtained from Iowa State University, Department of Computer Science, Ames, Iowa, 50011-1041, USA, probably via www.jmlspecs.org or the SourceForge project page for JML www.sourceforge.net/projects/jmlspecs.
This document provides the following information:
Except for the papers for which copyright is assigned to others (notably the paper in the directory docs/kluwer), and the runtime libraries, JML is copyrighted as open source software under the GNU general public license. See the file COPYING.txt in this directory for details.
The runtime libraries and their sources, including the specifications of the Java Development Kit (which become part of the runtime libraries), are copyrighted using the GNU Lesser general public license. See the file LesserGPL.txt in this directory for details.
JML is provided without warranty of any kind. See the files COPYING.txt and (for the runtime libraries and JDK specifications) LesserGPL.txt for details.
If you have problems, please look in the TROUBLESHOOTING section below. See also the HTML page JML.html in this directory for the documentation included in the release and other helpful documentation. If those steps don't help, please contact us by using the SourceForge tracking system to file a bug report, support request, or feature request. We will respond as soon as we're able to help you.
The current release has a type checker (jml), a tool (jmldoc) that produces web pages, a run-time assertion checking compiler (jmlc), a tool for running applications compiled with the run-time assertion checking compiler (jmlrac), and tools for use with JUnit (jtest, jmlunit, jml-junit, and jmlrac). The checker and works on JML input files found with suffixes
.refines-java, .refines-spec, .refines-jml, .java, .spec, and .jml,
and which may refer to refinements in other files with suffixes
.java, .spec, .jml, .java-refined, .spec-refined, and .jml-refined.
Directions for running it are below.
The instructions below are for users of JML releases, which are precompiled. (If you are a developer of JML, or if you want to work from the sources, then read the docs/developer-tips.html file for installation of a developer's version of the JML tools.)
You'll need Java (or the Java runtime environment, jre) to run the checker and the assertion checking compiler (jmlc). We've tested it with J2SDK version 1.4.1 and JDK 1.4.2.
Note that the tools do not work currently with JDK 1.5. If you try to use JDK 1.5 with the tools, you will get strange errors. We recommend that you uninstall JDK 1.5 before using the JML tools, unless you are very familiar with how to manipulate shell scripts, the Java CLASSPATH, etc. (We are planning to fix this in the future.)
Unless you're using Mac OS X, you also need to have the tools.jar file from the J2SDK 1.4.1 or J2SDK 1.4.2. This file is found in the lib directory in J2SDK 1.4.1 and 1.4.2; it's needed to run jmldoc. Our experience is that later versions of the tools.jar don't necessarily work. Users on Mac OS X apparently don't have to worry about this if they have updated to J2SDK 1.4.1 or later, as the equivalent is in their boot class path.
If you have the J2SDK 1.4.1 or J2SDK 1.4.2 tools.jar available, and if you're not on a Mac OS X running at J2SDK 1.4.1 or J2SDK 1.4.2, then you need to copy the tools.jar file from the Java install's lib directory into the Java install's jre/lib/ext directory. This makes it so that the tools.jar file can be found automatically by the jmldoc tool. On Mac OS X, you must run either J2SDK 1.4.1 or J2SDK 1.4.2, as the Mac OS X version of Java puts the tools.jar file in the equivalent of the boot class path, where it cannot be overridden.
If, when you start the JML launcher you have a problem with jmldoc starting, then you should be sure that the tools.jar file is copied to the jre/lib/ext in the Java runtime environment that is being used when you open (double click) on a jar file. On Windows machines, this may be under Program Files\Java\ as opposed to where you may have installed the J2SDK itself. That is, you need to copy the tools.jar file both into the J2SDK's jre/lib/ext directory and in the Java runtime environment's lib/ext directory. On Windows, you can look at the file types accessible by starting the Windows explorer on a directory on your local machine, then clicking on "Tools", then "Folder Options...", then selecting the "File Types" pane, and finding the entry for the "JAR" extension. Then click on "Advanced" (near the bottom right), select the "open" action in the "Edit File Type" window that pops up, and click on the "Edit..." button to the right. This pops up a window ("Editing action for type ...") that will show, in the second box, labeled "Application used to perform action:"), the program that is used to start jar files when you open them. It will be something like "C:\Program Files\Java\j2re1.4.2\bin\javaaw.exe ...". In such a case, you need to copy the tools.jar from your Java install (the J2SDK) to C:\Program Files\Java\j2re1.4.2\lib\ext.
Now, unpack the tar file in which you found this. For reference below, let's assume that you did
c: cd \ tar -xzvf temp\JML.tar.gz
This would make a directory named c:\JML containing the release. When you see c:\JML mentioned below, substitute the actual directory name for that (e.g., /usr/local/JML).
The simplest way to use the JML tools is to make a shortcut (or link) to the file JML\bin\jml-release.jar on your desktop or "start menu". If you then open this shortcut (e.g., by double clicking), then you will get the JML launcher, which can be used to run the tools. Be sure to the CLASSPATH from the options for each tool you are using, and usually it must include an absolute path to the specifications directory of the release, which is c:\JML\specs in our example.
This works on any platform in which you have Java installed and for which opening the jml-release.jar file runs the Java virtual machine on it, as in the command java -jar jml-release.jar.
Note that the jmldoc tool will only launch if you have copied the tools.jar file into the extensions directory, as described above.
If you are happy with the launchers, and if you don't want any other installation of command-line scripts for running the tools, then you are done with the installation.
See the Running Programs Compiled with jmlc section below on how to run programs with class files that result from compilation with the JML compiler (jmlc) that is availble from the launcher.
If you are on Unix (or a clone like Linux, or Cygwin), then you can use the script in bin/Install-JML-Scripts to install the shell scripts for running the various JML tools. If you are on Linux, or Unix (but not cygwin), and you installed into /usr/local, then execute the following command (as root).
/usr/local/JML/bin/Install-JML-Scripts
This will also install the manual pages in /usr/local/man.
If you are using cygwin on a windows machine, we also recommend installation into /usr/local, and in that case instead of the above command, execute the following (in the bash shell).
INSTALLTYPE=cygwin /usr/local/JML/bin/Install-JML-Scripts
Alternatively, you could run a command such as the following.
INSTALLTYPE=cygwin JMLDIR=/cygdrive/c/JML /usr/local/JML/bin/Install-JML-Scripts
Otherwise, either edit the bin/Install-JML-Scripts, or look at it to see what other options it supports.
The directory you install into should be on your PATH, so your shell can find these scripts. For example, if you install into /usr/local/bin, then you have to make sure that /usr/local/bin is on your PATH. In that case you should also be sure that /usr/local/man is in your MANPATH.
See below for details on using the command line scripts.
If you have Windows 98, ME, 2000, or XP, and you are not using cygwin, but you still wish to use a command line interface to the tools, the follow the rest of the directions in this section. If this applies to you, then copy from JML\bin all of the files that end in .bat to a directory on your PATH. (These files include jmlenv.bat, jml.bat, jml-gui.bat, jmlc.bat, jmldoc.bat, jmlrac.bat, jmlunit.bat, jml-junit.bat, jtest.bat, etc.) Then edit the copied file jmlenv.bat files changing JMLDIR to the correct value for you (whatever c:\JML really is, maybe d:\JML or something).
You may also need to adjust the properties of jml.bat and the other scripts to increase the environment space available to them.
See below for details on using the command line scripts.
To run the jml checker, from a command prompt, execute
jml file1.java file2.jml
for whatever your files are.
Note that you can also pass directories to jml, and it will check whatever files there are in that directory with the suffixes ".refines-java", ".refines-spec", ".refines-jml", ".java", ".spec", and ".jml". You can, for example, execute:
jml .
To use the run-time assertion checker, use the jmlc script, for example:
jmlc -Q .
See the Running Programs Compiled with jmlc section below on how to run programs with class files that result from compilation with jmlc using the jmlrac script.
Consult the manual pages for details on running the documentation generation tool jmldoc, and other JML tools.
HTML versions of the script manual pages are available from the file JML.html in this directory. If you installed as above on Unix or cygwin, then nroff versions have also been installed above. Plain text versions can also be found in the directory JML/docs/man/ (i.e., docs/man/ under this directory.
If you like to use info to read documentation, instead of HTML or PDF, then you can install the makeinfo-generated info files by copying the files named JML/docs/*/*.info* to a directory such as /usr/local/info, or whereever you keep such files.
To run Java programs where some (or all) of the class files have been compiled with the JML compiler (jmlc), you will need to have the classes compile in your Java CLASSPATH. However, just having these classes in your CLASSPATH is not enough.
In addition to the compiled class files, you have to run a jmlc-compiled program with JML/bin/jmlruntime.jar in the interpreter's boot class path, and with either JML/bin/models.jar or JML/bin/jmlmodelsnonrac.jar in your CLASSPATH. (The latter is somewhat faster in execution time, but does no dynamic checking on calls to the JML model classes.)
In addition, if you are using jmljunit-generated code, you also need to have JML/bin/jmljunitruntime.jar in your CLASSPATH.
There is a script file (and batch file) for doing all of this easily. This script is called jmlrac. You would use it instead of the normal Java virtual machine (java), as follows.
jmlrac my.package.name.ClassnameOfMain
where ClassnameOfMain is the class name of the class containing your program's main method, and my.package.name stands for the name of the package where ClassnameOfMain is found.
See the manual page for jmlrac for details and more examples of how to run programs using it.
After installation, please sign up for the mailing list jmlspecs-releases@lists.sourceforge.net through its SourceForge.net web interface. This will let us inform you of future releases.
We are also interested in your feedback on JML: things you like, don't like, find confusing, etc. Since JML is open source, we'd appreciate it if you'd send us any bug fixes or enhancements you are willing to share with others. See the SourceForge tracking interface for the jmlspecs project for places to file bug reports, support requests, patches, and feature requests for JML and its tools.
General discussions of this sort about JML can be sent to the JML interest mailing list at jmlspecs-interest@lists.sourceforge.net, once you subscribe to that mailing list. To subscribe, use the SourceForge web interface for the jmlspecs-interest mailing list.
Make sure that Java (e.g., the J2SDK) is installed first. If you use a version of the J2SDK other than 1.4.1 or 1.4.2, then you'll also need to have the J2SDK 1.4.2 (or 1.4.1) tools.jar available (found in the lib directory in J2SDK 1.4.2 and 1.4.1) to run the documentation generation tool, jmldoc. The easiest way to do this is to also install the J2SDK 1.4.2 (or 1.4.1) from java.sun.com. Then follow the directions above regarding the tools.jar file.
If the jmldoc tool doesn't work from the launcher, be sure you are using J2SDK 1.4.2 (or 1.4.1) to run the launcher; currently this doesn't work with other versions of Java. If that's not the problem, see the directions above regarding the tools.jar file, in particular the paragraph about making sure that you have copied the tools.jar file into the JRE install.
The tools don't work currently with Java 1.5 (also known as Java 5) or later versions of Java. If you have both Java 1.5 and 1.4.2 (or 1.4.1) installed, and if you are experiencing difficulties, please uninstall Java 1.5 first, and then try to fix your installation problems. Afterwards, you can reinstall Java 1.5, as long as you make sure that the JML tools are run using Java 1.4.2 (or 1.4.1). However, it is easier to debug problems with your install if you are not simultaneously having problems getting the right version of Java to run the tools. Be sure to test the JML tools you use after you reinstall JDK 1.5, if you do that.
If you get an error message like the following from the tools,
Cannot throw "java.lang.IllegalArgumentException" it does not inherit from "java.lang.Throwable" [JLS 11.2]
then this may mean that you are running the tools with Java 1.5 instead of 1.4.2 (or 1.4.1) as required. See the paragraph above for how to troubleshoot this problem.
If you're using command line scripts, be sure that these scripts are installed in a directory on your PATH and are executable.
For a Windows command line, make sure that you have edited the jmlenv.bat file copy that you placed in a directory on your PATH.
If you are using the Windows command line and edited the scripts, but still get a message like "The system cannot find the path specified" when you run them, it may be that the jmlenv.bat file still refers to directories that are not present at runtime. This may happen in a networked installation. To fix this, make sure that the jmlenv.bat file refers only to directories that will exist on the user's machine when it is run.
The following shouldn't happen anymore, but just in case... If you're working under Windows, be sure that the "\r\n" (^M^J) sequence is used to end each line of the jml.bat file. If you read it in under wordpad, make it look right and save it then it should be ok. If need be, remove the @echo off at the start of jml.bat and see what's going on. Conversely, on Unix, if you are having problems running the scripts it might be that the line endings are Unix style (use dos2unix if you have that to fix it).
Many errors are the result of misconfiguration of the tools, especially with respect to the CLASSPATH. The symptom that your CLASSPATH is incorrect is that you will get a java.lang.NoClassDefFoundError when you try to run the checker. If you can launch all the tools except for jmldoc, then you have a problem with the tools.jar file; see the instructions above to fix it.
Another CLASSPATH problem occurs if you have multiple copies of the java.lang classes, such as String on your CLASSPATH. The symptom of this problem is that JML tools complain about overriding methods such as toString with a different return type, when you are not changing the return type at all. The problem here is that the different copies of the java.lang classes on your CLASSPATH cause the JML tools to think that these are different types.
We haven't used JML with Jakarta's Ant build tool much. But Joe Kiniry reports that, since error messages are given with relative file names by the JML tools, it works best to run the JML tools from the top of one's directory structure.
If you have other troubles in the installation, please let us know by filing a support request through the SourceForge tracking system so we can try to help you.
@(#) $Id: README.html,v 1.38 2006/01/18 22:33:24 leavens Exp $