[JSR308] A simple proposal for recursive annotations
Dr. James J. Hunt
jjh at aicas.com
Wed Jun 17 18:24:37 EDT 2009
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
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
> > 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.
I plan to be at the meeting in Dagstuhl.
Dr. James J. Hunt * CEO aicas group * Tel: +49 721 663968 22
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
More information about the JSR308