Downloads

OpenJML is a tool for working with logical annotations in Java programs. It enables static or run-time checking of the validity of the annotations, with other features underway.

The tool is available as a standalone command-line application for MacOS and Linux (Ubuntu 18.04 and 20.04), with Windows Cygwin in progress.

Installing OpenJML (Command Line Tool)

The OpenJML command line tool is OS-dependent. Download the appropriate release from the github latest release page.

The download retrieves a .zip file. Unzip the file into a new directory of your choice (call it $OJ). After unzipping, $OJ should contain the `openjml` executable and other files and folders. Some browsers or download utilities will automatically unzip the .zip file for you, leaving an unzipped folder in your downloads folder. You can move or rename the folder (with all its contents) to a location of your choice.

These are the particularly relevant files in the top-level of the installation folder:

  • openjml -- the javac-like tool that does (static) deductive verification, compiles a Java program with runtime assertion checks, and other functions.
  • openjml-java -- a build of Java (java-21-ga as of 2023) but with JML libraries included, helful for running RAC-compiled Java programs
  • jmlruntime.jar -- the JML runtime files needed when executing Java files with runtime checks compiled in
  • OpenJMLUserGuide.pdf -- a copy of the reference manual for the OpenJML tool
  • JML_Reference_Manual.pdf -- a copy of the JML (language) reference manual
  • openjml-compile -- this script compiles a Java program that uses openjml capabilities programmatically
  • openjml-run -- this script runs a program compiled by openjml-compile

Current versions of the pdf file are also available from this web site.

If $OJ is the installation directory, then you can run openjml using the command line $OJ/openjml. For example, $OJ/openjml --version will emit the version number of this build.

Further instructions about running OpenJML can be found here.

SMT solvers

OpenJML uses SMT solvers as logic checkers. A selection of supported solvers is bundled with the OpenJML release.