[JSR308] A simple proposal for recursive annotations

[Joseph Kiniry]

On 25 Jun, 2009, at 20:08, Lex Spoon wrote:

> On Jun 24, 2009, at 10:08 PM, Gary T. Leavens wrote:
>> On Wed, 24 Jun 2009, Lex Spoon wrote:
>>> On Jun 17, 2009, at 5:01 PM, Joseph Kiniry wrote:
>>>> This is the approach that the JML community is now taking with  
>>>> JML6, using "JML Code Contracts."
>>>> James, you need to speak with either myself (as a partner in  
>>>> CHARTER), Gary (as JML head-cheese), or, better yet, Patrice or  
>>>> Robby (as co-leaders of the JML6 effort) so as to better  
>>>> understand what the next generation JML toolsuite, on which I  
>>>> plan on doing CHARTER tool development, will look like.
>>>
>>> To clarify, is the plan for JML 6 to move over to Java  
>>> annotations, or are you saying that the JML language will be even  
>>> more Java-like?  Is there any publicly available information on  
>>> that, or is it too early?
>>
>> There is still some debate in the JML community as to the approriate
>> input syntax for JML, but my vote definitelly against using Java
>> annotations for all of JML syntax.  However, it is attractive for  
>> many
>> purposes, particularly modifiers (such as @Pure, @SpecPublic, etc.),
>> and I believe we will move to using that kind of syntax for such
>> limited purposes.  There are several things keeping us from using  
>> Java
>> annotations for all of JML's annotations, in particular:
>>
>> - the need to encode arguments as strings,
>> - the need to pass along multiple similar annotations inside an  
>> array literal,
>> - the lack of statement annotations (for loop invariants, and variant
>>                                      functions for loops).
>
>
> I guess I am lost.  Joseph, what did you mean when you said "this is  
> the approach the JML community is now taking"?  It sounds like the  
> JML group is not using any form of extended Java annotations, and is  
> still having some constraint due to not having a good way to encode  
> expression-like content in the arguments to Java annotations.

I guess I am being too optimistic based upon our inaugural JML Spec-a- 
thon meeting in Tacoma that related to this topic.
   http://formalmethods.insttech.washington.edu/specathons/inaugural/

Hopefully, this week at our Dagstuhl seminar we'll resolve these  
issues, as Gary, Patrice, Robby, and James are all here (among others).
   http://www.dagstuhl.de/de/programm/kalender/semhp/?semnr=09292

Our whole day today focused on tool foundations, so there have been  
plenty of arguments about the pros and cons of using Java annotations,  
either in their current form or in a slightly extended form desired by  
our sub-community, for our new tool foundations.

We may come out of this meeting with some proposed patches to the JSR  
308 compiler.

Joe