OpenJML Development Environment Setup

David Cok edited this page May 30, 2018 · 35 revisions

Setting up an OpenJML development environment

The following instructions set up a clean development environment for OpenJML. These instructions are for the Eclipse development environment; they will need to be adapted by the developer for other environments.

Install Java

Because OpenJML uses OpenJDK, it turns out that you must develop the OpenJML for Java 8 with a Java 8 compiler and runtime environment. (Similarly you must have Java 7 to work on OpenJML for Java 7, which uses OpenJDK for Java 7). All new development is being applied to Java8.

So install the appropriate versions of Java on your machine. It is acceptable to have multiple versions present, though then you have to tell Eclipse which to use, in the list of installed JREs under the Java Preferences. Releases of Java can be obtained from OpenJDK (http://openjdk.java.net/projects/jdk8u/) or Oracle (http://www.oracle.com/technetwork/java/javase/downloads).

Install Eclipse

If you want to use Eclipse as your Java IDE, follow the instructions here.

Create an OpenJML working copy from github

The OpenJML source code resides in several repositories on github. Within a working copy, clones of these repositories are expected to reside in a specific relationship to each other. There are two simple means to create this structure.

You may need to clean and rebuild all the projects after they have been constructed in Eclipse.

Using Git commands directly

This option allows you to have the repository clone and working copy of the code separate from the Eclipse workspace itself. This is the recommended approach has it permits easily using the same working copy with shell commands or another IDE.

  • Create and cd to a new directory (designated $OPENJML) that will hold the working copies
  • Execute the commands
    git clone https://github.com/OpenJML/OpenJML.git
    git clone https://github.com/OpenJML/JMLAnnotations.git
    git clone https://github.com/OpenJML/OpenJMLDemo.git
    git clone https://github.com/OpenJML/Specs.git
    git clone https://github.com/OpenJML/Solvers.git
  • If you are going to be creating releases of OpenJML then you also need clones of these repositories:
    git clone https://github.com/OpenJML/OpenJML-UpdateSite.git
    git clone https://github.com/OpenJML/SMTSolvers.git
    Note that SMT Solvers are supplied in the 'Solvers' project.

Then link to those clones within an Eclipse workspace by doing the following steps:

  • Start Eclipse in a new workspace
  • Activate the File >> Import... menu command
  • Select General >> Existing Projects into Workspace, and click Next
  • Enter the path to the $OPENJML directory above as the root directory
  • Make sure that all the projects are selected
  • Click Finish
  • Enable Project >> Build Automatically and then Select Project >> Clean (for all projects) to clean and re-build the workspace

Using Eclipse to create clones within an Eclipse workspace

This option creates a github clone, working copy and all the relevant Eclipse projects directly within a Eclipse workspace. This technique may fail to produce a buildable environment if an instance of the OpenJML plugin is already installed in the Eclipse instance being used.

  • Start Eclipse with a new workspace of your choice.
  • Activate the File >> Import >> Team >> Team Project Set menu command
  • Enter the URL: https://raw.githubusercontent.com/OpenJML/OpenJML/master/openjml-master.psf
  • Click Finish and wait for the download to complete
  • Enable Project >> Build Automatically and then Select Project >> Clean (for all projects) to clean and re-build the workspace

Structure of the development environment

Either of the above creates the following projects in your Eclipse workspace:

  • JMLAnnotations - Definitions of Java annotations used by JML
  • OpenJDK - The snapshot of OpenJDK currently used
  • OpenJML - The core software of OpenJML
  • OpenJMLDemo - Some demo material
  • OpenJMLFeature - The Eclipse Feature plugin for the OpenJML Eclipse plugin
  • OpenJML-UpdateSite - The staging area for release builds of the OpenJML plugin
  • OpenJMLGUITests - Not yet used
  • OpenJMLTest - Test material for OpenJML
  • OpenJMLUI - The core software of the OpenJML Eclipse plugin
  • Specs - JML specifications of the Java system libraries
  • Solvers - SMT solvers usable by OpenJML
  • SMTSolvers - The Eclipse feature for the Solvers plug-in
  • vendor - A vendor branch for OpenJDK

To use the current development version of OpenJML, set the OpenJML and Specs projects to the 'development' instead of 'master' branch.

Optional: Create the openjml.properties file

You can customize your environment by creating a openjml.properties file. This file contains property definitions that are then the defaults, overriding any built-in defaults. For example, this mechanism can be used to set default command-line options. The openjml.properties file can reside in the current working directory or in your home directory or in the OpenJML installation directory.

  • Create the openjml.properties file by copying $OPENJML/OpenJML/OpenJML/openjml-template.properties to openjml.properties.
  • Once created, edit it, providing property definitions in the usual property name = property value format, typically without spaces.

Running OpenJMLTest within Eclipse

This is a good check to make sure your environment is set up correctly. To run the tests, choose the menu item Run >> Run Configurations.... Select the category for JUnit tests, and doubleclick on OpenJMLTest.

It will be obvious if the setup is incorrect; keep an eye on the console output. There are a few thousand tests; they take several hours to run. There are a number (typically < 50) tests that do not succeed; these are tests for fixes in progress or features not yet implemented.

Running OpenJML tests as a command-line task

Be sure that 'ant' and 'java' are available on your $PATH and that $JAVA_HOME is properly set.

In the OpenJMLTest directory, run the command ant -f build_OpenJMLTest.xml -Declipse.home=/path/to/eclipse cleanall build OpenJMLTest || exit 1 in which '/path/to/eclipse' is replaced by the absolute path to the Eclipse installation directory (i.e., the directory that contains the eclipse executable or, on a Mac, Eclipse.app). The results of the tests are contained in HTML pages in OpenJMLTest/junit.

Clone this wiki locally
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.
Press h to open a hovercard with more details.