printlogo
http://www.ethz.ch/index_EN
Welcome
 
print
  

JML2 Eclipse Plug-In

Open Positions

We are recruiting PhD students in program verification, programming languages, and programming environments. Check out the job descriptions.

Student Projects Available

Our group offers many different topics for Master's theses, Bachelor's theses, and Research in Computer Science Projects. 

Our Mailing List

If you are interested in our activities, you can subscribe to the PMInterest mailing list.

Workshop on Software Correctness and Reliability

All information on the workshop 2014 can be found here.

The slides and videos of 2013 are available on the workshop website

Overview


This Eclipse plug-in provides a basic integration of the Common JML2 tools into the Eclipse IDE.

Originally, this plug-in started as a small part of the Universe type system inference tools, but was spun off later. See the research page for an overview of the Universe type system and the tools page for information about the tools we provide.

Installation

Add the URL

http://www.pm.inf.ethz.ch/research/universes/tools/eclipse/

as an update site to Eclipse. Then search for new plug-ins and install the JML2 Eclipse plug-in. We provide two Eclipse "features": the main plug-in for all tools and a help plug-in. These two are independent of each other and can be installed as needed.

Requirements

The plug-in was developed using Sun Java 6 and Eclipse 3.4.1 on Linux. However, the plug-in and the included JML2 were compiled to Java 5 bytecode and should therefore run with an older JVM.

Basic Usage

After successful installation, you will find the following changes: 1) a "JML2 Tools" context menu and toolbar buttons, 2) a "Run As -> JML Rac" configuration, and 3) "JML2 Plug-in" properties page in the project properties.

In the "Project Explorer", the context menu for files and folders contains a "JML2 Tools" sub-menu with three commands: 1) "Run JML2 checker" executes the static type checker and 2) "Run JML2 compiler" checks the code and then compiles it with runtime assertion checking (RAC). 3) "Run JML2 exec" checks the code and then compiles it with the JML exec tool.

Code that has been compiled with RACs can be executed with "Run As -> JML Rac". If a runtime check fails the exception is printed in the "Console" view.

The project properties contain a "JML2 Plug-in" page that sets the command line options for the checker and the compiler.

The toolbar can be enabled by selecting the "Window -> Customize Perspecitve..." menu, then selecting the "Commands" tab and then enabling the "JML2 plug-in toolbar" option.

The default keyboard shortcuts can be changed by selecting the "Window -> Preferences..." menu, then selecting the "Keys" tab under "General" and then configuring the "JML2..." entries.

See the JML2 documentation and examples for details about JML.

Feature Summary

Screenshots

mail-small
mail-small
props-small
props-small
help-small
help-small

Open Issues


Also see the "JML2 Eclipse plug-in" category in the SF Tracker. Please add any bugs and feature requests there.

Tested Environments


Version 1.1.0 was successfully tested in the following environments:

Contact


These tools are provided as-is without any support or warranty. The source code for the plug-ins is contained within the respective JAR files. The source code for MultiJava and JML2 are available from their respective web sites. Also see the GNU General Public License, version 2.

Werner M. Dietl

Release History

Release History

Version 1.1.1, November 5th 2008:

Version 1.1.0, September 22nd 2008:

Version 1.0.9, August 8th 2008 (08.08.08):

Version 1.0.8, July 20th 2008:

Version 1.0.7, July 16th 2008:

Version 1.0.6, July 14th 2008:

Version 1.0.5, February 2008:

Version 1.0.4, October 2007: Small improvements.

Version 1.0.2, March 2007: Improvements during the master project of Andreas Fürer

Version 1.0.0, Summer 2006: Semester project of Paolo Bazzi

 

Wichtiger Hinweis:
Diese Website wird in älteren Versionen von Netscape ohne graphische Elemente dargestellt. Die Funktionalität der Website ist aber trotzdem gewährleistet. Wenn Sie diese Website regelmässig benutzen, empfehlen wir Ihnen, auf Ihrem Computer einen aktuellen Browser zu installieren. Weitere Informationen finden Sie auf
folgender Seite.

Important Note:
The content in this site is accessible to any browser or Internet device, however, some graphics will display correctly only in the newer versions of Netscape. To get the most out of our site we suggest you upgrade to a newer browser.
More information

© 2015 ETH Zurich | Imprint | Disclaimer | 29 October 2012
top