[JSR308] A simple proposal for recursive annotations

Dr. James J. Hunt jjh at aicas.de
Fri Jun 5 20:10:46 EDT 2009

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.


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

More information about the JSR308 mailing list