Re: Joe-E 2.0 Release

On 3/11/08, David Wagner <[email protected]> wrote:
> 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).

I think it would be good if the Joe-E verifier checked all Java
projects in the workspace for packages with the @verified annotation
and turned on verification for those packages. With only one switch,
the programmer, and the reviewer, can be confident that if the
@verified annotation is present, the code is being verified.

If you have some spare cycles, adding a graphical annotation to
verified packages in the Workspace view would be nice (similar to the
way subclipse does). Or maybe the inverse should be done, graphically
annotating Java packages that are not Joe-E verified, to make them
stand out.

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

Would the Joe-E verifier consult the .safej files, or the Policy
class? I prefer the latter, so that the programmer can abandon the
Joe-E toolset, other than the Joe-E library, if need be. Consulting
the Policy class also ensures that the compile time behaviour is
consistent with the runtime behaviour, which is a good thing. This
implementation would also mean the verifier could run without a taming
directory being configured. That configuration setting would only be
needed if the programmer wanted to generate a new Policy class.

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

I'd skip this feature. I like that the verifier is read-only and won't
touch my code under any circumstances.

Once you've got your first package-info.java file, you can propagate
it to another package with a simple copy-paste operation. Eclipse is
smart enough to update the contents of the file to match the new
package.

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

I think these changes would work for me.

Thanks,
--Tyler