[JSR308] Annotations on statements (and expressions?)

[Gary T. Leavens]

Hi Tom and all,

JML of course doesn't absolutely *need* support from Java for JML, and
has done fine without direct support.  One can of course add custom
attributes to class files to record information, which works.

The reason that JML would *like* support from Java for *syntax* is to
make it easier to create tools to process (small) subsets of JML's
notation, by writing contract syntax in Java annotations.  Of course
we can get by without this, and do currently.  However, it seems that
having a syntax based on annotations for JML or similar languages
would have positive benefits for tool builders.  On the other hand, if
we can't use annotations uniformly for all assertions and contracts,
in particular for loop invariants, then I would say that the pain of
annotations (having to put everything in string literals) is not worth
it for JML, as then JML would be even more non-uniform in its syntax
than it already is.  In that case I would argue that JML should make
no or very little use of annotations.

I thought this JSR was about syntax for adding annotations to more
places in Java.  Specification language contracts on statements (and
loops in particular) are one instance of that.  So that is why I've
presented another use case for loop/statement annotations.  You may of
course not think that's compelling, but I certainly do, and I wanted
to add it to the mix of other reasons for adding annotations on
statements.

On Wed, 31 Jan 2007, Tom Ball wrote:

> I don't understand why a language like JML needs support from Java. There's 
> no need to turn Java into an intermediate language, as JVM class files 
> (should) already address that need.  The JVM and Java core classes make a 
> great platform for researching new languages, and with the open-source 
> release of javac it is now even easier to create them.  If the JVM spec needs 
> to be improved to support better specification then either this JSR should 
> focus on that issue, or a new JSR should be created.
>
> Tom
>
> Gary T. Leavens wrote:
>> 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
>> 
>> 
>> _______________________________________________
>> JSR308 mailing list
>> JSR308 at lists.csail.mit.edu
>> https://lists.csail.mit.edu/mailman/listinfo/jsr308
>
>
> _______________________________________________
> JSR308 mailing list
> JSR308 at lists.csail.mit.edu
> https://lists.csail.mit.edu/mailman/listinfo/jsr308
>


         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