[e-lang] Joe-E 2.0 Release

[Tyler Close]

On Sat, Mar 8, 2008 at 6:10 PM, David Wagner <daw at cs.berkeley.edu> wrote:
> 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.

It looks like the Joe-E library can be updated to use this proposal by
simply adding the last 3 lines below to
org.joe_e.reflect.Reflection#safe():

    static private boolean safe(final Member member) {
        final Class declarer = member.getDeclaringClass();
        if (declarer.getPackage().isAnnotationPresent(verified.class)) {
            return true;
        }
         ...

--Tyler