Software Download
Yoonsik Cheon | HOME


JET | JML4c | UTJML | BibPHP | JML

JML4c Overview | Download | Documentation

Executable JAR Files

The following two JAR files contain an executable JML4c compiler (jml4c) and a runtime library, respectively; both are compiled with JDK 1.6.

To run jml4c, use the -jar option of the java command; e.g., type the following line on the command prompt. 

  [Unix] java -jar jml4c.jar -cp "jml4c.jar:." Sample.java
  [Cygwin] java -jar jml4c.jar -cp "jml4c.jar;." Sample.java

Or add jml4c.jar to your CLASSPATH and excute the Main class, e.g., 

  java org.jmlspecs.jml4.rac.Main Sample.java

Here is a shell script, jml4c.sh, that does this automatically.

To run the compiled bytecode file, say Sample.class, use any JVM provided that jml4rt.jar was added to your CLASSPATH (or use the -cp option for that); e.g., type the following line on the command prompt. 

 java Sample

Here is a shell script, jml4.sh, that automatically adds jml4rt.jar to the CLASSPATH and invokes the JVM.

Sample JML file and Output

Here is a sample Java class, Account.java, annotated with JML specifications. If you compile and run it, you should receive an output similar to the following: 

[Cygwin] jml4c Account.java
[Cygwin] jml4 Account
Exception in thread "main" org.jmlspecs.jml4.rac.runtime.JMLInternalPrecondition
Error:
By method Account.withdraw
Regarding specifications at
  File "Account.java", line 27, character 16
With values
  amt: 200
  bal: 100

        at Account.main(Account.java:36)
Java Source Code

You can browse and download JML4c specific Java source code directly from the SVN repository; to download the entire source code including the front-end and the Eclipse Java compiler, refer to its jml4c.psf file.

To compile the source code, refer to the JML4c installation instructions. The main class is org.jmlspecs.jml4.rac.Main which is a subclass of org.eclipse.jdt.internal.compiler.batch.Main; refer to its API specification. The whole API specifications are available from the Documentation page.

Last modified: $Id: download.php,v 1.8 2014/09/09 22:52:55 cheon Exp $