Software Download Yoonsik Cheon | HOME	JET | JML4c | UTJML | BibPHP | JML

JML4c Overview | Download | Documentation

These notes are intended for local JML4c developers. You first need to configure Eclipse and then download JML4c source code including the front end and the Eclipse Java compiler. For this, follow the following steps.

Getting and Setting Up Eclipse

• Obtain the latest 3.4.0 version of Eclipse (not 3.4.1 or later) from here.
• Install the Subclipse, e.g., using the update site: http://subclipse.tigris.org/update_1.6.x; Subclipse is an Eclipse plug-in providing support for Subversion. Some of JML4c source code are stored in Subversion repositories.

Setting Up the Workspace

Configure Eclipse to use Java 6 by doing the following steps whenever a new workspace is created.

• Ensure that the default Java runtime for Eclipse be JDK 1.6
• Ensure to have Java 6 JDK installed. Note that it is a JDK, not a JRE.
• Select the check box for the jdk1.6 so that it will be used by default.
• Ensure that the compiler compliance level be set to 1.6.

Downloading the JML4c source code

The easiest way to download JML4c and all the files including the JML4 front end and the Eclipse Java compiler is to:

• Download the jml4c.psf project set file.
• Import this project set file using File >> Import ... Team >> Team Project Set.
  • When asked for a login and password for the dev.eclipse.org pserver, use login "anonymous" and an empty password.

Verifying the installation

To verify the workspace, run JML4 test cases, JML4RAC test cases, and optionally Eclipse test cases.

• Select the org.jmlspecs.eclipse.jdt.core.tests project from the Java perspective's Project Explorer tab.
• Open the project and navigate to:

  org.jmlspecs.eclipse.jdt.core.tests >> src >> org.jmlspecs.eclipse.jdt.core.tests

• Right click RunJml4Tests.java and select Run As >> JUnit Test.
• Note that test results, as of Jan. 26, 2010, expect:
  • Windows and Mac OS X/Intel: 8 error and 190 failures out of about 3193 tests.

• Select the org.jmlspecs.eclipse.jdt.core.tests project from the Java perspective's Project Explorer tab.
• Open the project and navigate to:

  org.jmlspecs.eclipse.jdt.core.tests >> src >> org.jmlspecs.eclipse.jdt.core.tests.rac

• Right click >AllTestSuites.java and select Run As >> JUnit Test.
• Note that test results, as of Jan. 26, 2010, expect:
  • Windows and Mac OS X/Intel: 8 error and 121 failures out of about 2633 tests.

• Select the org.eclipse.jdt.core.tests.model project from the Java perspective's Project Explorer tab.
• Open the project and navigate to:

  org.eclipse.jdt.core.tests.model >> src >> org.eclipse.jdt.core.tests >> RunJDTCoreTests.java.

• Right-click on the java file: Run As >> JUnit Plug-in Test.
• Note that test results, as of Feb. 20, 2008, expect:
  • Windows and Cygwin: 1 error and 22 failures out of about 25000 tests.
  • Linux: 1 error and 22 failures out of about 25000 tests.
  • Mac OS X/PPC: 17 errors and 69 failures out of about 25000 tests.
  • Mac OS X/Intel: 1 error and 37 failures out of about 25000 tests.

Last modified: $Id: install.php,v 1.5 2010/01/29 03:35:27 cheon Exp $