Java Modeling Language (JML) Wiki

Status: Beta

Brought to you by: chalin, cheon, davidcok, dmzimmerman, and 3 others

OpenJmlSetup

Labels:

Authors: Anonymous

OpenJML Setup
- Obtaining and Installing Java

OpenJML Setup

These notes are intended for JML developers willing to test and/or contribute to the OpenJML project.

You need to do the following tasks (described in more detail below) in order to create a development environment for OpenJML:

install Java (1.7 or later) on your system,
install Eclipse (4.2 or later, with all current updates from Eclipse) on your system,
obtain and install a copy of the Yices prover (if you want to do static checking),
configure Java for your system and Eclipse workspace,
configure bash for your system,
create a set of Eclipse projects containing the OpenJML source,
inform OpenJML about your local system,
compile OpenJML,
build and test an OpenJML release, and
run the OpenJML JUnit tests.

Note that Eclipse generally requires a significant amount of memory to perform well. Development mostly occurs under Cygwin on Windows 7; some testing occurs on Mac 10.6.8; feedback on experience with Unix or MacOSX or raw Windows platforms or your Cygwin configuration is welcome.

Obtaining and Installing Java

Eclipse will require Java 1.5 or later. This can be the version of Java that is generally installed on your system.
OpenJML requires Java 1.7 or later. This can be a version of Java that is simply referenced as an "installed JRE" by Eclipse.
I am currently developing with Java 1.7.0_07 downloaded from Oracle.

Obtaining and Configuring Eclipse

OpenJML is being developed with Eclipse 4.2.2 (or perhaps later versions by the time you read this). Though the tool was previously developed using earlier versions of Eclipse (as far back as 3.4 at least), we do not test the development environment on older versions of Eclipse and the plug-in code now uses some 4.2 features. Both the 32-bit and 64-bit versions of Eclipse are operational (with the respective versions of Java).

Download Eclipse from: Eclipse Builds or Eclipse Packages pages. I use the Classic package.
Install the Subclipse plug-in, e.g., using the update site: http://subclipse.tigris.org/update_1.8.x.
On a Windows system, Eclipse may be launched either from Windows directly (if Java is installed on Windows) or from from a bash shell in Cygwin (in which case the JAVA_HOME and PATH variables need to be set appropriately so that the java, jar, and bash executables can be found). The umask should be set to 022.

You will likely need to increase the memory allocations for Eclipse, in the eclipse.ini file within your Eclipse distribution. I am currently using

-XX:MaxPermSize=512m
-XX:PermSize=512m
-Xms512m
-Xmx2048m

Configuring Java for your Workspace

Every time you create a new installation of Eclipse, you must ensure you have a Java 7 or later JRE installed and set as the JRE associated with the JavaSE-1.7 Execution Environment.

Configuring bash for your Workspace

The release build and test process currently uses bash. [ GNU make is no longer used by OpenJML; bash is being transitioned to ant, but this transition is not yet complete. ] bash is invoked by ant; ant expects to find bash on the $PATH; some utility scripts expect bash at /bin/bash.

Obtaining and Configuring Prover(s)

You only need to install provers if you will be doing static checking. Currently OpenJML works with Z3 (version 4.3 on Windows), and Yices 2 (version 2.1) on Mac or Windows. I have not tested on Linux.

For Yices

Go to the download page. Fetch a copy of Yices 2.1 for your platform.
Put the prover in a convenient place in your file system.
You will need to edit the openjml.properties file to record the absolute path to the Yices executable, once you have obtained the OpenJML source code from SourceForge, as described below. On Windows, at least, the syntax of the path must be of the form C:/Java/yices-1.0/yices.exe. Note the combination of Windows prefix and UNIX file separators.

For Z3, follow the steps above, but for Z3 version 4.3 from http://z3.codeplex.com/.

Obtaining and Compiling a Working Copy of OpenJML

Before performing this step, the appropriate JRE must be installed in Eclipse and associated with the JavaSE-1.7 Execution Environment.

The OpenJML source code and development environment is contained in a SourceForge subversion repository. For more information about JmlSpecs subversion access, see here.

The easiest way to load OpenJML and all of the required test files in Eclipse is to:

import the project set file using File >> Import ... Team >> Team Project Set; when asked for the URL to a project set file, use the URL

http://jmlspecs.sourceforge.net/OpenJML-projectSet.psf ;

this will create a number of (currently 8) related projects in your Eclipse workspace; it is convenient to put them all in one Working Set;
clean and rebuild all projects;
If you find you need to reinstall OpenJML from scratch, simply commit all changes you want to keep, delete all the OpenJML-related projects, including the on-disk contents, and re-import the projects using the project set file.

The above procedure is easy, but it creates the various Eclipse projects directly within the Eclipse workspace. Many developers prefer to keep the Eclipse projects separate from the Eclipse workspace. An alternate setup procedure is the following:

Choose a directory in which the OpenJML projects are to reside, e.g. OpenJMLProjects. A subdirectory will be created in this directory for each of the OpenJML projects (i.e. there will be subdirectories JMLAnnotations, OpenJDK, OpenJML, ...)
cd to that directory and issue the svn commands found at http://jmlspecs.sourceforge.net/svn_commands (these commands are obtained simply by an appropriate text transformation of the projectSet file).
Now open Eclipse using a workspace into which you want to import the projects you have just created. The workspace directory should be different than the directory used above.
Choose File -> Import -> General -> Existing Projects into Workspace
Browse to the directory OpenJMLProjects (or whatever directory you used to contain the Eclipse projects obtained from SVN above). All the OpenJML projects will appear in the Projects box. You can leave them all selected, though you likely will not need the vendor project.
Click Finish - do not use Copy projects into workspace
Now do a clean and rebuild of all of the OpenJML projects simultaneously (to be sure they are built in the correct order).

Additional Local Configuration

The OpenJML development environment needs to know some things about your local environment. That information is placed in the openjml.properties file within the OpenJML project. A fresh install will not have such a file, as you create one by copying and editing the openjml-template.properties file, also contained at the top level of the OpenJML project. Follow the documentation in that file to know which properties to set. As an example, which must be tailored to your system, my openjml.properties file has these settings:

openjml.localSetup=
openjml.defaultProver=yices
openjml.prover.yices=C:/cygwin/home/dcok/apps/yices-1.0.29-i686-pc-mingw32/yices-1.0.29/bin/yices.exe
openjml.prover.z3=C:/cygwin/home/dcok/mybin/z3.exe

Your local version of openjml.properties should not be committed to source code control. However, when you update your development environment from SourceForge, you should check that openjml-template.properties does not have new contents that you need to reflect in your copy of openjml.properties.

Running the JUnit tests

The JUnit tests are run using the OpenJML - Test launch configurations. These are found under the Run toolbar button. The first time it is run, you may need to find it under the JUnit section of the Run Configurations.

Some of the JUnit tests run static checking tests and thus require that a prover be set in openjml.properties.

Detail: One of the JUnit tests (!testSourcePath4) checks the use of a runtime library in the file jmlruntime.jar. This jar file is created when a release is built (as described in the next section). If no release is built, that test will simply emit a message saying the file is not present; otherwise the version of jmlruntime.jar that was most recently built is used. If the jml runtime library is under active development, the file will need to be rebuilt frequently.

Building a Release

A command-line tool release is built as follows:

ensure that the openjml.properties file is created and edited appropriately as described above;
ensure that the JRE is appropriately set as described above;
ensure that all projects have compiled correctly and all JUnit tests pass;
execute the Eclipse External Tool configuration named Build OpenJML Release. A console window will report progress and show any errors. The first time you run this launch configuration, you may need to find it under the External Tool configurations, in the group of Ant Builds;
the created release is contained in a file named openjml-VERSION-REVxxxxx.tar.gz, where 'VERSION' is a date in 'yyyymmdd' form, and xxxxx is the current SVN revision number, e.g., openjml-20111031-REV1234.tar.gz. Repeated release builds on the same day without commits to SVN will overwrite previous tar files. Release builds from previous days will accumulate in your workspace until you delete them by hand. They are not committed to subversion unless they are publicly announced releases.

The instructions for publishing a release (including the Eclipse plug-in) to the public web site are part of the sourceforge source files at https://sourceforge.net/p/jmlspecs/code/HEAD/tree/OpenJML/trunk/OpenJMLFeature/README. Please communicate with the OpenJML lead developers before you even start to think about doing this.

Testing a Release

To test a release, first build it and then perform this step. Note that a release test only performs a set of straightforward 'smoke' tests to ensure that the release contains the requisite files and performs basically correctly. The separate set of JUnit tests checks the functionality more completely.

Run the Eclipse External Tool configuration named Test OpenJML Release. A console window will report progress and show any errors. Note that this launch configuration tests the release with the most recent time stamp.

The release build and test steps can be performed successively using the Eclipse External Tool configuration named Build and Test OpenJML Release.

Building and publishing the OpenJML Eclipse plug-in files

The instructions for building and publishing a release (including the Eclipse plug-in) to the public web site are part of the sourceforge source files at https://sourceforge.net/p/jmlspecs/code/HEAD/tree/OpenJML/trunk/OpenJMLFeature/README.

_If there is a way to automate these steps, please share it! _

Note: at present some parts of the release (the pdf of the user guide) are only available in David Cok's environment, so others should not publish releases.

Wiki: OpenJml