[e-lang] Joe-E 2.0 Release

[Bill Frantz]

daw at cs.berkeley.edu (David Wagner) on Tuesday, March 11, 2008 wrote:

>6. We could add a convenience feature to the Eclipse plugin that
>automatically emits a @verified annotation for packages in which the
>Joe-E verifier has successfully verified every class in that package.
>This could be optionally enabled or disabled according to user
>preferences.  Programmers who don't want to use this feature can
>type in the one-line @verified annotation into the package-info.java
>file by hand.  Joe-E programmers who don't care can have the Eclipse
>plugin auto-generate it for them, so they don't need to know anything.

What happens if a package is successfully verified, and has the
annotation, and then is changed so it will not verify? Is the
annotation removed?

Cheers - Bill

-------------------------------------------------------------------------
Bill Frantz        | The first thing you need when  | Periwinkle
(408)356-8506      | using a perimeter defense is a | 16345 Englewood Ave
www.pwpconsult.com | perimeter.                     | Los Gatos, CA 95032