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.

I met with Adrian yesterday, and we both think this is a great suggestion.
Thanks very much for the excellent feedback.

So, let me recap the proposal as I think I understand it, and I'd love to
get feedback from you on whether it would help address the problems you've
been running into -- and feedback from anyone else with an interest.

1. Joe-E programmers would normally put their Joe-E code into
separate packages that contain only Joe-E code.  They would add
the @verified annotation to those packages.  The Policy class would
then allow reflection on any member that comes from a package with
a @verified annotation, or any member that is listed in the Java
taming database.

2. The Joe-E verifier would presumably need to ensure that, if it
is run on a package with the @verified annotation, then it has or will
run the verifier on every class within that package.

3. It's someone else's problem to ensure that packages that the
Joe-E verifier will be run on every package with the @verified
annotation (or, conversely, that if the Joe-E verifier is not run
on some package, someone else must ensure that the package does not
contain an @verified annotation).

4. We would still have .safej files that contain our database of
taming decisions for legacy Java classes.  We would build a tool that
reads those .safej files and auto-generates a Policy.java file.  The
standard Policy.java file could be distributed with Joe-E, so for
Joe-E programmers who don't want to modify or extend the Java taming
database (i.e., don't want to modify or add .safej files), they could
use the standard Policy class.  Programmers who want to extend the
standard taming database would modify .safej files and then run the
auto-generator tool to generate a custom Policy.java file for them.

5. Joe-E would no longer generate .safej files for Joe-E code.
This would ensure that Joe-E remains a verifier and does not require
code generation facilities.  .safej files would only be needed for
Java code (e.g., Java class libraries, or any Java code that you
write that you want to be able to reflectively access from within
Joe-E code).

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.

7. Mixing Joe-E and Java code within the same package would not be
well-supported.  Or, more specifically, if you mix Joe-E and Java
code in the same package, Joe-E code will not be able to reflectively
invoke or access any of the Joe-E code in that package.  That seems
okay (and could perhaps be addressed if it is a serious issue).

I think this would be a nice simplification to the design and would bring
the Joe-E verifier's status back in line with a pure static verifier.
It would also support applications that are split up into multiple
Eclipse projects, like Waterken, in a nicer way.  We could still
support applications, like Waterken, that are built out of both Joe-E
and Java code.  And it would ensure that Waterken could dynamically load
new Joe-E code at runtime without needing to restart Waterken or refresh
its taming database.

I realize that this proposal omits your suggestion to eliminate .safej
files entirely.  We should discuss that some more if you think that'd
be a good addition.

What do you think?  I know Joe-E 2.0 created a bunch of frustrations
for you; would this address those frustrations?