[JSR308] A simple proposal for recursive annotations

[Gary T. Leavens]

Hi Lex and all,

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).

That said, there is considerable interest in using Java annotations to
encode JML for intermediate representations, and as alternative input
syntaxes, so any added power, in particular the above 3 points, would
be welcome.

You can see a study of a possible way to encode JML annotations in
terms of Java annotations in the following papers by my former student
Kristina Boysen Taylor:

Kristina B. Taylor, Johannes Rieken, and Gary T. Leavens. Adapting the
Java Modeling Language for Java 5 Annotations. Department of Computer
Science, Iowa State University, TR #08-06, April 2008.
ftp://ftp.cs.iastate.edu/pub/techreports/TR08-06/TR.pdf

Kristina B. Taylor. A Specification Language Design for the Java
Modeling Language (JML) Using Java 5 Annotations. Department of
Computer Science, Iowa State University, TR #08-03, April 2008.
ftp://ftp.cs.iastate.edu/pub/techreports/TR08-03/TR.pdf

          Gary T. Leavens
          439C Harris Center (Bldg. 116)
          School of EECS, University of Central Florida
          4000 Central Florida Blvd., Orlando, FL 32816-2362 USA
          http://www.eecs.ucf.edu/~leavens  phone: +1-407-823-4758
          leavens at eecs.ucf.edu