[JSR308] Annotations on statements (and expressions?)

[Ted Neward]

I get a little worried about the verbosity and figurative (if not literal)
fragmentation of Java when we start going down these roads. I'm not debating
the usefulness of such a construct, mind you--just its appropriateness for
Java, as opposed to a new language running on the JVM.

Ted Neward
Java, .NET, XML Services
Consulting, Teaching, Speaking, Writing
http://www.tedneward.com
 

> -----Original Message-----
> From: jsr308-bounces at lists.csail.mit.edu [mailto:jsr308-
> bounces at lists.csail.mit.edu] On Behalf Of Gary T. Leavens
> Sent: Tuesday, January 30, 2007 7:11 PM
> To: Neal Gafter
> Cc: jsr308 at lists.csail.mit.edu
> Subject: Re: [JSR308] Annotations on statements (and expressions?)
> 
> 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
> 
> --
> No virus found in this incoming message.
> Checked by AVG Free Edition.
> Version: 7.5.432 / Virus Database: 268.17.15/659 - Release Date: 1/30/2007
> 9:31 AM
> 

-- 
No virus found in this outgoing message.
Checked by AVG Free Edition.
Version: 7.5.432 / Virus Database: 268.17.15/659 - Release Date: 1/30/2007
9:31 AM