JMLE

jmle − compile JML annotated files into executable (.class) files

jmle [option] ... file-or-directory-or-package [file-or-directory-or-package] ...
The command jmle compiles JML class specifications contained in Java and JML specification files into executable prototypes of the specified classes. Any Java(TM) code in method bodies is ignored - only the specifications of methods are compiled. The output is .class file(s), which can be treated in much the same way as the output of any java compiler. Note, however, that the .class files produced by jmle depend on classes in the org.jmlspecs.jmlexec package, which therefore also need to be loaded. These can be obtained from the file JML/bin/jml-release.jar in the JML release. The JML release provides the script jmlre which adds this jar file to the CLASSPATH and then runs java, which facilitates this loading process. As the JML specifications are translated to constraint programs, the resulting executables are significantly slower and use much more memory than would be typical of hand-coded implementations of the same specifications.

The class files produced by jmle can be mixed with those generated by other Java compilers. However, the specifications of all superclasses and implemented interfaces (except for standard Java(TM) and JML library classes and interfaces) must be compiled by jmle , either prior to compiling the class specification of interest or all together (on the same command line). Similarly, if a specification uses instances of classes other than standard Java(TM) or JML library classes, the specifications of those classes must also be compiled with jmle . For refinement chains, only the file in the chain containing the specification that you wish to execute should be compiled using jmle . Usually, this would be the last file in the chain, but it need not be if you do not wish to execute all specifications in the refinement chain.

The jmle script sets the CLASSPATH and then runs the Java class org.jmlspecs.jmlexec.Main, which does both syntax and type checking of Java and JML files, and then generates the JVM bytecode in class files for each of the Java files (i.e., for each .java or .jml file).

If the compiler finds an error, the file name, line number, and column number where the error occurred are reported. In such cases, by default, processing stops and no output will be produced for the files.

For a tutorial introduction on the basics of using jmle, see the EXAMPLES section below.

The jmle script supports the options described below. 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.

−−debug, −c

Produces (copious) debugging information. The default is not to produce this information. Additionally, when the executable generated from the specification is run, a complete trace of all constraint handling rules used in executing the specification is printed. The entire constraint store and the bindings of all logic variables are printed each time a constraint is considered for simplification, so the trace can become quite large.

jmle also inherits many of the options of jmlc . For details, see jmlc(1).

The typical way to compile a specification for execution is as follows.

jmle Test.jml

This produces Test.class, which can be treated as ordinary JVM bytecode. That is, you can write, compile and run ordinary Java code that creates instances of class Test and uses those instances to call the methods of class Test.

To run programs compiled with jmle you need to have various runtime classes in your CLASSPATH. The jmlre(1) script provides a way to do this automatically. See its manual page for more details.

The CLASSPATH environment variable is used to find Java class and source files, as well as JML specification files.

The jmle 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.

jmlre(1), jmlc(1), jmlrac(1), java(1), javadoc(1), jml(1), jmldoc(1), jmlunit(1), jtest(1)

[1] B. Krause and T. Wahls. "jmle: A tool for Executing JML Specifications via Constraint Programming". In L. Brim, editor, Formal Methods for Industrial Critical Systems (FMICS ’06), volume 4345 of Lecture Notes in Computer Science, pages 293 - 296. Springer-Verlag, 2006. http://users.dickinson.edu/~wahlst/papers/tool.pdf

[2] N. Catano and T. Wahls. "Executing JML Specifications of Java Card Applications: A Case Study". In preparation.

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