[JSR308] A simple proposal for recursive annotations

[Joseph Kiniry]

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.

> 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