Re: Joe-E 2.0 Release

Bill Frantz <[email protected]>
Newsgroups gmane.comp.lang.e.general
Message-ID <r02010500-1049-0D0EB7ADEFAD11DCB7FC0030658F0F64@[192.168.1.5]>
[email protected] (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
lmpx.com only provides a reader for public news (NNTP) servers. It is not affiliated with the servers or forums shown here and is not responsible for the content of articles, which is written by their respective authors.