[JSR308] A simple proposal for recursive annotations

[Jonathan Aldrich]

As I think I've written to this list before, adding recursive 
annotations--ideally in the simplest possible way--would be an enormous 
gain in the power of the annotation system, which right now is 
relatively hobbled.

In addition to JML-style specifications, most lightweight, "type 
annotation" style static checking systems require some kind of 
parameterization, which requires recursive annotations to do right 
(because the annotations in the static checking system may be 
parameterized in different ways than Java type parameterization).  Other 
use cases, like capturing database queries and persistence information, 
would definitely also benefit from recursive annotations.

I think your proposal sounds reasonable.  I'd love to see an 
implementation of something like this that can be used to demonstrate a 
wide variety of use cases (as in your JML example and those I mention 
above) and to show that there are no technical "gotchas."

Jonathan


Dr. James J. Hunt wrote:
> 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
>