[e-lang] Joe-E 2.0 Release

[Adrian Mettler]

I may have been unclear.  The plan would be to keep the UI widget, but 
to remove the existing mechanism for storing the enabled/disabled state. 
The toggle would just be a way to indicate the presence of the flag in 
the package-info.java file, which would be the authoritative 
specification consulted by the verifier.  It would also toggle the flag 
in the file (potentially creating the file if it doesn't already exist), 
but only if clicked on.  My hope is to use an Eclipse JDT API for 
adding/removing the annotation rather than hacking on the file directly, 
  which should be more likely to do the right thing.

In terms of a name for the annotation, how about something like 
org.joe_e.IsJoeE? (or isJoeE -- I've noticed that you prefer to have 
lowercase annotations, but Sun uses the same casing convention as 
classes; does anyone know which convention is more common?)
Alternately, one could use something more general like 
org.joe_e.safe/Safe, which would be consistent with use on trusted 
library code that isn't actually Joe-E (such as the Joe-E library, or 
non-verified components of Waterken).  This would have the advantage of 
decreasing the size of the taming database and reducing somewhat the 
need to use a non-canonical taming db.

-Adrian

Tyler Close wrote:
> On Tue, Mar 11, 2008 at 7:43 PM, Adrian Mettler
> <amettler at cs.berkeley.edu> wrote:
>>  For Joe-E code, the verifier can use the @verified annotation to
>>  determine what packages to verify.  This will allow the specification of
>>  which packages in a project are Joe-E code to be persisted when the
>>  project is exported (the persistent properties that I am currently using
>>  for this purpose are not, which is less than ideal)  The drop-down
>>  toggle that enables and disables verification can instead turn on and
>>  off the annotation.
> 
> I'm nervous about the toggle button rewriting my code and/or getting
> into a different state than the @verified annotation. Could we get rid
> of the toggle and just use the @verified annotation as the switch for
> turning the verifier on and off, so the Joe-E verifier simply monitors
> the package-info.java file for the presence of this annotation?
> 
> --Tyler
> _______________________________________________
> e-lang mailing list
> e-lang at mail.eros-os.org
> http://www.eros-os.org/mailman/listinfo/e-lang