ESCJava2PluginExplanation

WikiInclude(ESCJava2PluginDescription)

The Extended Static Checker for Java version 2 (ESCJava2) is a programming tool that attempts to find common run-time errors in JML-annotated Java programs by static analysis of the program code and its formal annotations. Users control the checking that ESCJava2 performs by annotating their programs with specially formatted comments called pragmas.

ESC/Java2 is available in two forms:

• ESC/Java2 as a command-line tool with a simple Swing GUI front-end, or
• ESC/Java2 as an Eclipse plugin.

This latter, plugin-based version of this subsystem has several features that deeply integrate it into the Mobius PVE.

With respect to environment configuration, its preferences system is integrated into the PVE at the IDE-level and at the project-level. The former supports configuration at the systems-level, the latter settings specific to a project that are saved with the project.

Focusing on use, the integration with development is transparent. Each time a file is saved the extended static checker is run in the background asynchronously. Thus, from the developer point of view, warnings and errors appear as regular Eclipse markers on lines of code and as run underlines within program code and specifications. Likewise, all developer feedback appears within the appropriate Eclipse Warning'' and ''Error panes. The extended static checker is also executed manually on a variety of different constructs (on a package, a class, a method, etc.) with a single mouse action.

Version: 2 Time: Mon Apr 26 16:27:20 2010 Author: kiniry (kiniry) IP: 130.226.133.55