[JSR308] An implementation of Subtyping for Annotations

[Joseph Kiniry]

James, Michael, et al.,

I want to voice our wholehearted support for this effort, both from my  
research group as well as in the larger community in which I work  
including the JML community and the MOBIUS project.

Our existing verification efforts will be significantly enhanced if we  
have the ability to embed specification languages into Java  
annotations at the source and bytecode level, and such necessitates  
the support for recursive annotations.  Subtyping of annotation types  
I had always thought was a no-brainer, so when the initial annotation  
support came out in Java5 I was quite surprised that it was missing.   
Perhaps this gives us an opportunity to clean up quite a bit of the  
design mess resulting from that decision.

In particular, if this functionality were to be adopted by JSR 308, we  
plan on revising the MOBIUS bytecode subsystem[1], which is based upon  
BML[2], so that, instead of using unused opcodes to encode structured  
assertions (i.e., pre- and postconditions, invariants, etc.) in  
bytecode (which causes problems across VMs and requires quite a bit of  
infrastructure), we would instead use a revised subset of the JML  
annotations we have already written for experimentation in writing JML  
specifications with annotations[3].

Best,
Joe

[1] https://mobius.ucd.ie/trac/wiki/ByteCodeSubsystem
[2] http://www-sop.inria.fr/everest/BML/
[3] http://jmlspecs.svn.sourceforge.net/viewvc/jmlspecs/JMLAnnotations/

On 6 Aug, 2009, at 19:56, Dr. James J. Hunt wrote:

> Dear Michael,
>
> I am glad that I finally have some funding to support the 308  
> effort.  I
> will ask Christian to make the patch.  We will also look at  
> implementing
> line or block level annotation.  That is the reason why I tried to
> access the page today.  Is there some other way to get the last  
> version
> of the specification that was there?
>
> Sincerely,
> James
>
> P.S. Yes, it did get throw, but not until I sent it out again.  I had
> cross posted it to the JML group and there it did fail to get posted.
>
> On Thu, 2009-08-06 at 09:40 -0700, Michael Ernst wrote:
>> James-
>>
>>> Please find access information for obtaining an extension of the  
>>> JSR 302
>>> Javac which supports Annotation subtyping below.
>>
>> Thanks for doing this.  The only way to get new features in (like  
>> this one
>> that the list has been discussing for many years) is for someone to  
>> take
>> the lead with an implementation.
>>
>> Can you make a patch to either the JSR 308 compiler or to the OpenJDK
>> compiler (the patch would be the same either way), rather than to  
>> the JSR
>> 302 compiler?  That would be more useful to people on this mailing  
>> list.
>>
>>> P.S. This is a resubmission, since the original included the code  
>>> as an
>>> attachment and was therefor too large.
>>
>> I'm not sure what gave you this impression, butler It looks like your
>> original message went through:
>>
>>  https://lists.csail.mit.edu/pipermail/jsr308/2009-August/000648.html
>>
>>                    -Mike
> -- 
> Dr. James J. Hunt      * CEO aicas group       * Tel: +49 721 663968  
> 22
>
> aicas incorporated
> 69 West Rock Ave.      * New Haven, CT 06515   * USA
> http://www.aicas.com   * Tel: +1 203 676 9807  *
>
> Business Filing Number: 0002879819, State of Connecticut
> President: Dr. James J. Hunt, Secretary/Treasurer: David P. Reddy
>
> aicas --- allerton interworks computer automated systems GmbH
> Haid-und-Neu-Straße 18 * D-76131 Karlsruhe     * Deutschland (Germany)
> http://www.aicas.com   * Tel: +49 721 663968 0 * FAX: +49 721 663968  
> 99
>
> USt-Id: DE216375633, Handelsregister HRB 109481, AG Mannheim
> Geschäftsführer: Dr. James J. Hunt
>
>
> _______________________________________________
> JSR308 mailing list
> JSR308 at lists.csail.mit.edu
> https://lists.csail.mit.edu/mailman/listinfo/jsr308