[JSR308] Annotations on statements (and expressions?)

[Tom Ball]

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