ESC/Java2 Summary
The Extended Static Checker for Java version 2 (ESC/Java2) 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 can control the amount and kinds of checking that ESC/Java2 performs by annotating their programs with specially formatted comments called pragmas.
ESC/Java2 is available in three forms.
- ESC/Java2 is built into the Mobius Program Verification Environment
- ESC/Java2 is a command-line tool with a simple Swing GUI front-end. One can download source and binary versions of this version via our download page.
- ESC/Java2 is also an Eclipse 3.5 plugin, available through the Mobius PVE update site. Development of the plugin is also hosted in the Mobius Trac.
Feedback
The Mobius Trac server hosts development of ESC/Java2. One can browse the source, checkout a development snapshot, track commits, and browse feature requests and bug reports, and file such tickets (registration and login mandatory) via this system.
There are two mailing lists that focus on ESC/Java2:
- The JMLSpecs-ESCJava mailing list is the "users" mailing list where one can ask questions of experienced users and the developers of ESC/Java2. Subscribe to this list by registering at SourceForge.
- The ESCJava-Developers list is used by ESC/Java2 developers to discuss new features, bugs, designs, research, etc.