OriginalJMLPluginExplanation

The very first Eclipse plugin supporting JML was created by developers at Kansas State University working in tandem with the core JML tool developers, then at Iowa State University. This basic plugin was developed, in part, so that JML developers could gain experience with Eclipse plugin development. This plugin is called JMLEclipse.

JMLEclipse permits an Eclipse user to specify, via standard Eclipse mechanisms, how and when various programs in the core JML tool suite are used on a per-project basis. In particular, the JML checker jml and compiler jmlc can be manually and automatically triggered. Additionally, within the standard Java editor, JML specifications are specially highlighted; e.g. JML keywords are in a special typeface and/or typestyle.

Unfortunately, JMLEclipse is now only a historical artifact. JMLEclipse is no longer used because it only works with Eclipse version 3.0, now several years old. This restriction is due to the manner in which JMLEclipse was developed: it was too tightly integrated with the core of Eclipse.

JMLEclipse shipped with early internal test versions of the Mobius PVE, as they ran on Eclipse 3.0. So, while JMLEclipse no longer ships with the Mobius PVE, its feature set continues to influence the features of other JML subsystems.

Version: 1 Time: Fri Mar 28 14:49:07 2008 Author: dcochran (dcochran) IP: 193.1.132.32