[JSR308] A simple proposal for recursive annotations

[Chester Chen]

I don't know, I felt that annotations like this may be powerful,
but takes on its own trajectory: programming language withing program language.

The code will become so cluttered with annotation we lost the 
cleanness of the code and program logic become too hard to comprehend.

Certain level of annotations are helpful, but too much become ..., well, too much.

my two cents.



-----Original Message-----
From: jsr308-bounces at lists.csail.mit.edu on behalf of Dr. James J. Hunt
Sent: Fri 6/5/2009 5:10 PM
To: jsr308 at lists.csail.mit.edu
Subject: [JSR308] A simple proposal for recursive annotations
 
Dear Colleagues,

Here is a proposal for recursive annotations that are powerful enough to
be able to express preconditions, postconditions, and invariants a la
JML.  Recoding JML in annotations is beyond the scope of this JSR, but
some examples of possible encodings are presented for clarity.

Recursive types without subtypes does not work very well.  It is however
strange for a language that supports subtyping (in this case via
subclassing) to have a type refinement system that does not allow
subtyping.  The other solutions, using an empty annotation at the bottom
or even arrays.

If recursive annotations where to be supported, I would suggest doing it
via subtyping with only indirect direct recursion.  As for subtyping, I
would not allow a subtype to override an element ("method") of its
parent, just add new ones.  This is in keeping with the interface method
analogy and avoids certain obscure ambiguities in usage. (Java should
have done this with attributes that are not private as well.)  I would
also opt for single inheritance, since I do not seen any reason that
multiple inheritance is necessary.

For the expression example, one might then have something like the
following (of course this is an abbreviated JML encoding example).

public @interface Expression
{
}

/** JML expression */
public @interface Eval extends Expression
{
  public String value ();
  public Expression[] args() default {};
}

/** Java method */
public @interface Invoke extends Expression
{
  public String value ();
  public Expression[] args() default {};
}

/** JML function */
public @interface Function extends Expression
{
  public String value ();
}

/** Java locally variable */
public @interface Value extends Expression
{
  public String value();
}

/** int constant */
public @interface Int extends Expression
{
  public int value();
}

/** Array element */
public @interface Int extends Expression
{
  public String value();
  public Expression index();
}

/** JML special value */
public @interface Result extends Expression
{
}

public @interface Spec
{
  public Expression[] require() default {};

  public Expression[] assert() default {};
}

For example, a specification might be something like the following.

@Spec(require = [@Eval(value = ">=",
                       args = [@Value("i"), @Int(0)])
                 @Eval(value = "<", 
                       args = [@Value("i"),
                               @Invoke(value = "length",      
                                       args = [@Value("a")])],
      assert = [@Eval(value = "==",
                      args = [@Result,
                              @Element(value = "elements",
                                       index = @Value("i"))])
      

Yes, this would add some complexity, but the benefits would be large.
It might be preferable from a user point of view just to write an
expression in a string, but such a string would have no checking and
becomes uninterpretable when simply stored in a class file because the
parse context is no longer available.  Even here, parameter and local
variables references are challenging, so that it may be necessary to
write something a bit more complex.

It may turn out, that for JML this syntax hard to read.  That may be,
but one could still write JML in its current form and automatically
transform it to annotations.  That would still enable saving JML
information into the class files for processing at the byte code level.
Data follow analysis is a good example of a tool that could use this
information for verifying that method preconditions are always met.

Before tying having someone implement this, I would like to hear
feedback from the list.

Sincerely,
James

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

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


_______________________________________________
JSR308 mailing list
JSR308 at lists.csail.mit.edu
https://lists.csail.mit.edu/mailman/listinfo/jsr308

-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.csail.mit.edu/pipermail/jsr308/attachments/20090605/dce68dc5/attachment.htm