[JSR308] A simple proposal for recursive annotations

[Lex Spoon]

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.


Lex