Joe-E 2.0 Release

David Wagner 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.

Bill Frantz wrote:
> 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?

In that case, the Joe-E verifier will reject and the Eclipse
plugin will display at least one verification error.

I believe the burden is on the programmer to ensure that all Joe-E
code passes the Joe-E verifier.  I don't know if the Eclipse plugin
does anything else to protect users from this case, like forcing the
build to fail and deleting .class files.  Adrian could answer that.

I wonder if the name @verified is misleading.  Would a name like
@needsverification or @allegedlyjoee better convey the intent?  If I
understand Tyler's proposal correctly, this annotation is a message from
the programmer to the system indicating that the programmer intended
this code to be within the Joe-E subset, rather than a message from the
Joe-E verifier that the code has in fact been verified to be within the
Joe-E subset.  We can only rely upon @verified packages to have passed
the Joe-E verifier if (a) the user is careful to run the Joe-E verifier
on all packages that contain Joe-E code; (b) the user is careful not
to run the code if the Joe-E verifier flags any errors.

Does this sound overly dangerous?