#141 Allowing JML specs in Java5 annotations

[Arnout Engelen]

In the long run, it might be interesting to allow JML
annotations to be expressed not only as specially
formatted comments (i.e. /*@ requires foo; */), but
also as Java5 Annotations (i.e. @JML("requires foo;").

This might make parsing annotated code / tool support /
integration into tools easier (and thus more likely to
happen :) ).

Probably not something that can be done right now
though, as i think JML annotations are allowed in some
places where Java5 annotations are allowed (yet).

[Joseph Kiniry]

Logged In: YES
user_id=42011

Robby should chirp up and give his impressions of this use
of annotations. I think he has some pretty strong (and
negative) experiences with such.

I think that Curt's students may also experiment with this
option.

Personally, I think that Java 5's annotations are poorly
designed and implemented and, at the source level, are
inappropriate for rich annotations. On the other hand, the
annotation support at the bytecode level should be leveraged.

[Gary T. Leavens]

Logged In: YES
user_id=633675

Kristina Boysen, a student of mine, is actively working on
exploring how to do this for her master's thesis.
So I'm assigning this request to her, and in the future we
will see a proposal and tools about this.

For the record, Mark Utting also suggested something along
these lines quite a while (1/2 year?) ago.

Thanks.