[JSR308] Annotations on statements (and expressions?)

[Gary T. Leavens]

Hi all,

I wanted to point out another use for annotations on statements. For
our work on specifications with the Java Modeling Language (JML, see
http://jmlspecs.org), we would like to attach loop invariants to loop
statements.  This is actually my major reason for joining this JSR, as
it's the biggest failing of Java's annotations for our work.  For
example, we'd like to write:

    int i = 0;
    int sum = 0;

    @maintaining("sum == (@sum int j; 0 <= j && j < i; a[j])")
    while (i < a.length) {
       sum += a[i];
       i++;
    }

where the @maintaining annotation is attached to the while loop, and
the @sum is not an annotation, but just something in the string in the
annotation.

Another use for this is to attach entire contracts to describe the effect
of a statement (including loop statements), as this is often an aid to
provers.  For example, something like:

    @following(@spec_case(requires="i < Integer.MAX_VALUE",
                          ensures="i == @old(i + 1)"))
    inc(i);

(to take a very trivial example).  That's less important to us, but
would still be quite useful.

For JML we don't usually need annotations on expressions, but we could
definitely use annotations on new object construction expressions,
such as

     new @Rep Document()

I hope that something that could handle such examples would be
acceptable to the group and the JCP.  :-)

On Tue, 30 Jan 2007, Neal Gafter wrote:

> Annotations on statements?  Annotations on expressions?  It sounds like the
> scope of our work is exceeding the scope of the original proposal.
>
> I can imagine us wanting to support annotations on every sematically
> meaningful nonterminal in the language, but I'm not sure a result along
> those lines is likely to be acceptable by the JCP.
>
> On 1/30/07, Michael Ernst <mernst at csail.mit.edu> wrote:
>> 
>> Trevor-
>> 
>> Annotations on loops and other statements are within the scope of JSR 308,
>> as noted by the current version of the proposal.  However, no one has yet
>> put forward a specific technical proposal for the syntax of loop/statement
>> annotations (in Java and in the class file).  Once someone does so, then
>> we
>> can evaluate that proposal and accept, improve, or reject it.
>> 
>> I know that several other people, including Wayne Carr and Eugene Kuleshov
>> (who responded separately to your message), are also interested in this
>> topic.  Perhaps you could join forces in preparing a proposal or at least
>> preparing a statement that broaches the issues to the mailing list.

I'd be happy to help with such a proposal...

         Gary T. Leavens
         Department of Computer Science, Iowa State University
         229 Atanasoff Hall, Ames, Iowa 50011-1041 USA
         http://www.cs.iastate.edu/~leavens  phone: +1-515-294-1580