Joe-E 2.0 Release

Tyler Close writes:
>I've got an alternate proposal for marking Joe-E code.
>
>Java supports package annotations that are available at both compile
>time and runtime. I suggest Joe-E define an annotation
>org.joe_e.verified. To enable Joe-E verification of a package, the
>programmer adds the standard package-info.java file with content:
>
>@org.joe_e.verified package org.example.stuff;
>
>The Policy class can then check that a reflected member is either
>defined in a Joe-E verified package, or is enabled in the safej
>database. The safej database then doesn't need to contain any
>information about Joe-E verified code, only tamed Java code.

Interesting.  Thanks for the concrete proposal.  This sounds worth
mulling over.

Should we be concerned about the possibility that code could add an
@org.joe_e.verified annotation to itself without having been run through
the Joe-E verifier?  Or do you see a way to prevent that from happening?