ProgramVerificationEnvironmentUsage

As the Mobius PVE is simply an enriched version of Eclipse, Eclipse users will find the Mobius PVE quite familiar. This wiki page provides a high-level developer walk-through of the configuration and use of the Mobius PVE.

The Mobius PVE is available from this MOBIUS Trac server and via the KindSoftware research group website (the research group of the MOBIUS UCD partner), Pre-configured Eclipse builds are available for all main platforms including Microsoft Windows, Apple's Mac OS X, and Linux. Download the appropriate archive; it can be unpacked anywhere on the local disk.

A sample Eclipse workspace is also available from the aforementioned sites. This workspace includes example projects and documentation about the Mobius PVE.

Each main subsystems included in the current "gamma'" release of the Mobius PVE is configured separately. First one must create a new Java project, or import an existing Java project. One may also simply use an existing Eclipse workspace with the Mobius PVE.

The first subsystem that one should configure is the CheckStyle coding standard checker and the complementary Eclipse code formatter. The CheckStyle plugin is configured via the Project Properties dialog, available either via the Project menu or via a right mouse action on the project name in the resources browser.

If one wishes to further configure the default coding standard, either the configuration can be tweaked via the plugin's preferences panel, or one can duplicate and edit the external MOBIUS coding standard configuration file available from [https://mobius.ucd.ie/repos/websites/MobiusToolsWiki/Standards/CodeStandard/].

Configuring the Eclipse code formatter takes place in a similar fashion. The Mobius PVE is pre-configured with several code formatters.

The JML plugin is configured on a per-project basis. The JML typechecker, compiler, and runtime assertion checker are configured independently.

JML typechecking or compilation is currently accomplished via a menu action. In a future version of the Mobius PVE, autobuilders will be intelligently triggered instead.

Several static checkers are included in the Mobius PVE. First, configuring and executing the main static checker, ESC/Java2, is summarized.

The main static checker included with the Mobius PVE at this time is ESC/Java2. ESC/Java2 is configured via menu actions and preferences panels.

To initially configure the plugin, one must enable the ESC/Java2 "nature" (a set of configurations that ensures the plugin is properly configured for use) and "builder" (an action that is triggered at specified times, typically to build a system or to perform some analysis). The JML menu contains item to perform initial setup of the plugin.

Project-specific configuration of ESC/Java2 is accomplished via a Project Properties panel. Via this control panel, one controls all of the standard warnings for ESC/Java2, the use of various theorem provers, and programming language variants, including JavaCard.

The ESC/Java2 builder can be enabled to run each and every time a Java source file is saved. This is accomplished via another item in the JML menu.

Finally, ESC/Java2 can be manually executed on any project subunit (file, package, \etc) via a right mouse action on the appropriate resource.

Configuring plugins like PMD, FindBugs, Mylyn, EclEmma and Metrics all happen in the standard fashion. Decide which, if any, of the non-MOBIUS static checkers should be enabled as auto-builders. (An auto-builder is a builder that is automatically triggered when a specific action takes place, e.g. when a file is saved.)

As all plugins are pre-configured to compliment verification with MOBIUS subsystems, their preference settings should, in general, should be untouched.

Several other subsystems (the JML Folding subsystem, the MOBIUS Coq editor, the Umbra bytecode viewer, \etc) are configured in similar ways.

WikiInclude(PerformingVerification)

Version: 1 Time: Mon Mar 31 12:26:53 2008 Author: dcochran (dcochran) IP: 193.1.132.32