[JSR308] A simple proposal for recursive annotations

[Dr. James J. Hunt]

Dear Joe,

Certainly, the syntax Lex suggests in quite appealing.  What I am
concerned about it how this syntax can be encoded to be available in the
class file.  Nobody really wants to write the JML purely in annotation
syntax.

On Wed, 2009-06-17 at 23:01 +0200, Joseph Kiniry wrote:
> Hi James and Lex,
> 
> On 16 Jun, 2009, at 19:49, Lex Spoon wrote:
> 
> > On Jun 16, 2009, at 12:12 PM, Dr. James J. Hunt wrote:
> >> As for using Java syntax for annotations, that is perhaps  
> >> desirable, but
> >> more difficult to implement.  You example is too short for me to  
> >> see if
> >> what you intend would work for a specification language.  It would be
> >> nicer to write something like
> >>
> >> @Spec("\require i >= 0 && i < a.length();
> >>      \ensure \result == elements[i];")
> >
> >
> > My proposal was to embed the expressions directly, rather than in a  
> > string.  That way, it's the Java compiler that does the parsing and  
> > type checking.  It already has subroutines for that, so it can  
> > easily do so.  The annotation processor is then provided an abstract  
> > syntax tree.
> >
> > Presuming annotations worked that way, you could write the above  
> > spec like this:
> >
> > @Spec(require(i >= 0 && i < a.length()), ensure(result ==  
> > elements[i]))
> >
> > Doesn't that look sufficient?
> 
> 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.

I have tools that will need the same kind of information at the byte
code level, so having it readily available as annotations would be
helpful.

> > Note that several things must be in scope for this example to work,  
> > but it doesn't seem like any trouble.
> >
> > 1. "require", "ensure", and "result" must be in scope.  They could  
> > be imported from static members of a utility class.
> >
> > 2. "i" and "a" must also be in scope.  This initially struck me as  
> > weird, when I was first thinking about these problems for Scala, but  
> > over time I came around to allowing it.  It's just too common to  
> > want to annotate a method and talk about it's parameters.
> 
> > ...snip nice discussion on typechecking use of units...
> 
> > Overall, I had meant just to make a little suggestion, but I confess  
> > this is turning into a real proposal.  Where do things stand now?   
> > If there is really pressure to extend the annotation language to  
> > support things like preconditions, postconditions, and units, then I  
> > confess I really do propose using Java expressions.  It looks much  
> > better to me than the alternative of adding multiple extensions to  
> > the annotation language and still not having as much  
> > expressiveness.  I would be happy to help out, for example by  
> > contributing a reference implementation, but I will wait to hear  
> > where things are before putting any more time into it.
> 
> We are moving towards having a reference implementation at this moment  
> via JML6.  I suggest that CHARTER participants who are invested in  
> using JML as their annotation language join the team, so to speak.
> 
> Joe

I plan to be at the meeting in Dagstuhl.

Sincerely,
James

-- 
Dr. James J. Hunt      * CEO aicas group       * Tel: +49 721 663968 22

aicas incorporated
69 West Rock Ave.      * New Haven, CT 06515   * USA
http://www.aicas.com   * Tel: +1 203 676 9807  *

Business Filing Number: 0002879819, State of Connecticut
President: Dr. James J. Hunt, Secretary/Treasurer: David P. Reddy

aicas --- allerton interworks computer automated systems GmbH
Haid-und-Neu-Straße 18 * D-76131 Karlsruhe     * Deutschland (Germany)
http://www.aicas.com   * Tel: +49 721 663968 0 * FAX: +49 721 663968 99

USt-Id: DE216375633, Handelsregister HRB 109481, AG Mannheim
Geschäftsführer: Dr. James J. Hunt