Why shouldn't a qualifier apply to both types and declarations?

[Michael Ernst]

This has become a FAQ, so I have written a new FAQ for the Checker
Framework manual explaining it. Let me know if it is not clear.

-Mike



Why shouldn't a qualifier apply to both types and declarations?

It is bad style for an annotation to apply to both types and
declarations. In other words, every annotation should have a @Target
meta-annotation, and the @Target meta-annotation should list either only
declaration locations or only type annotations. (It's OK for an annotation
to target both ElementType.TYPE_PARAMETER and ElementType.TYPE_USE, but no
other declaration location along with ElementType.TYPE_USE.)

Sometimes, it may seem tempting for an annotation to apply to both type
uses and (say) method declarations. Here is a hypothetical example:

Each Widget type may have a @Version annotation. I wish to prove that
versions of widgets don't get assigned to incompatible variables, and
that older code does not call newer code (to avoid problems when
backporting).

A @Version annotation could be written like so:

@Version("2.0") Widget createWidget(String value) { ... }

@Version("2.0") on the method could mean that the createWidget method
only appears in the 2.0 version. @Version("2.0") on the return type
could mean that the returned Widget should only be used by code that
uses the 2.0 API of Widget. It should be possible to specify these
independently, such as a 2.0 method that returns a value that allows
the 1.0 API method invocations.

Both of these are type properties and should be specified with type
annotations. No method annotation is necessary or desirable. The best way
to require that the receiver has a certain property is to use a type
annotation on the receiver of the method. (Slightly more formally, the
property being checked is compatibility between the annotation on the type
of the formal parameter receiver and the annotation on the type of the
actual receiver.)

Another example of a type-and-declaration annotation that represents poor
design is JCIP's @GuardedBy annotation [GPB+06]. As discussed in Section
7.1.3, it means two different things when applied to a field or a
method. To reduce confusion and increase expressiveness, the Lock Checker
(see Chapter 7) uses the @Holding annotation for one of these meanings,
rather than overloading @GuardedBy with two distinct meanings.