[JSR308] Desire for Annotation Inheritance

Nels Beckman nbeckman at cs.cmu.edu
Sun Oct 5 12:43:57 EDT 2008


Hello members of JSR 308,

We are writing to let you know of our need for annotation inheritance that
would function much in the same way as that of Java classes. Kevin Bierhoff
and I are graduate students, working on static analysis for Java. In
particular, our program PLURAL attempts to statically verify correct usage
of type-state.

In order to control aliasing, so that our analysis can be modular, we use a
series of Java annotations on method signatures, in order to describe the
legal patterns of aliasing for the objects that are being passed to and
returned from each method. Here is an example:

@Full
void openSocket(@Immutable URL socketLocation) { ... }

The @Full annotation indicates that the receiver object can only be modified
via one program reference. The @Immutable annotation indicates that many
references will refer to the same object that socketLocation refers to, but
that none of them will be used to modify the URL.

Here are our problems:

First, we've got 10 annotations that are, for all intents and purposes,
identical.
@Full
@Immutable
@Unique
@Pure
@Share
@ResultFull
@ResultImmutable
@ResultUnique
@ResultPure
@ResultShare

Each of these annotations has the exact same fields. They differ only in the
"level" of aliasing "permission" they denote, and whether they describe the
return value or the receiver (see next point for more on this issue).

This is a major pain when we have to add/remove fields to/from these
annotations, because we have to make sure that we do the same thing for each
annotation. While we are aware that a restructuring of our annotations
could eliminate this problem (e.g., @Permission(Permission.Full) ), we are
not willing to add this additional burden on the users of our system. Our
annotations are burdensome enough as it is!

Here is our second problem, which we just alluded to:
Because there is only one spot on a method where we can put an annotation,
we are not able to distinguish syntactically between an annotation on the
receiver and an annotation on the return value. We solve this problem by
having a separate series of annotations for the result of a method call. We
have heard that your JSR intends to fix this problem by adding a separate
location where the method itself could be annotated. We would like to
express our support for such a measure.

Our final problem:
For technical reasons, users of our system may sometimes want to use an
@Perm annotation, which exposes the full generality of our system. This
annotation has two fields, one for the precondition and one for the
post-condition. At the moment, both of the fields are strings, which we
parse with an antlr parser in order to determine which permissions a user
desires. Here is an example:
@Perm(requires="full(this) in OPEN * pure(#0) in WAITING",
ensures="full(this) in CLOSED")

We would like to allow both requires and ensures to hold nested combinations
of annotations.  For example:
@Perm(requires=@Conjunction({@Full(arg="this",state="OPEN"), at Pure(arg="#0",state="WAITING")}),
ensures=@Full(arg="this",state="CLOSED"))

Unfortunately, because annotations cannot form a sub-typing relationship, we
are unable to give a type to the requires and ensures fields.  Notice that
we need to be able to arbitrarily combine annotations using annotations like
@Conjunction, @Disjunction etc., which forbids a solution using a simple
array.  Furthermore, sub-typing would allow us to use our atomic @Full,
@Immutable, etc. annotations in this more powerful setting, rather than
having to resort to a separate mechanism (which further complicates
annotation evolution).  Finally, the presence of both strings parsed into
and annotations directly representing our permissions means that our
infrastructure must first turn these two input formats into one common
representation, greatly reducing the value of having annotations be a part
of the Java language.

Allowing annotations for form a class hierarchy would solve this, and our
first problem, and we urge you to consider such a measure.

Thanks for your consideration.

Nels Beckman and Kevin Bierhoff
Carnegie Mellon University
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.csail.mit.edu/pipermail/jsr308/attachments/20081005/8b457754/attachment.htm 


More information about the JSR308 mailing list