PerformingVerification

Performing verification within the Mobius PVE is integrated directly into the standard practices of software development. All static checkers can be executed manually with a right mouse button action and/or a menu operation, typically at multiple levels of granularity (e.g. check a method, a class, a file, a package, etc.). Some static checkers like Checkstyle, PMD, FindBugs, and ESC/Java2 can also be configured as autobuilders, which are triggered each time a resource changes.

Verification conditions are generated by three different subsystems shipped with the Mobius PVE at the moment. VC generation from ESC/Java2 is built-in and VCs are only retained if special switches, currently unavailable via the Eclipse ESC/Java2 plugin, are used. VC generation with the MOBIUS direct VC generation is also only controlled via command-line tools at this time. Finally, as discussed in the aforementioned chapter, development of the VC generator for FreeBoogie is still underway.

The MOBIUS Prover Editor is an Eclipse "perspective". It is automatically loaded and initialized anytime a Coq theory file or proof script file is loaded within the Mobius PVE. No special configuration is necessary. If the prover needs to be reset, a small reinitialize button is available in the toolbar.

Finally, viewing and editing Java bytecode with Umbra is accomplished by simply opening a bytecode file. While viewing bytecode, a variety of buttons are available that permit one to refresh the view, jump to source corresponding to the currently selected bytecode fragment, etc.

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