Re: Joe-E 2.0 Release

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

Just a nitpick: if I understand correctly, this is an assertion that
the code is intended to be verifiable, not that it has been verified.

So, I think @org.joe_e.verifiable would a better name for the annotation.

-- 
David-Sarah Hopwood