@SuppressSubtypingWarning Implemented

@SuppressSubtypingWarning Implemented

I have now implemented @SuppressSubtypingWarning as far as I am going to, I think. I limited it only to methods and constructors; it can’t be applied to classes or interfaces. I think the impact would have been to unspecific.

There are several ways a method can acquire an annotation:

A method is annotated itself.
The same method in a superclass is annotated.
A class is annotated and the method is first defined in that class or a subclass.

More formally:

Let be an annotation.
Let be a method.
Let , , , be classes.
Let m(C) be the set of methods defined (i.e. introduced or overridden) in class .
Let a(C) be the set of annotations that are directly attached to class , i.e. that appear in front of ’s class definition.
Let a(C, m) be the set of annotations that are directly attached to method in class , i.e. that appear in front of ’s method definition in the class definition of .
Finallly, let annotations(C,m) be the set of annotations that are applied to a method in class , either because the method was directly annotated or because the annotations were somehow inherited.

A method in class has an annotation if one of the following statements is true: $A \in annotations(C,m)$ .

The definition of annotations(C,m) is:

$annotations(C,m) = \\\\<br /> \hspace{15mm}\\{ A : A \in a(C, m) \\} \cup \\\\<br /> \hspace{15mm}\\{ A : \exists S \text{ such that } C <: S, A \in a(S, m) \\} \cup \\\\ \hspace{15mm}\\{ A : \\\\ \hspace{30mm}\exists D \text{ such that } C <: D, m \in m(D) \wedge \\\\ \hspace{30mm}\exists S \text{ such that } D <: S, A \in a(S) \wedge \\\\ \hspace{30mm}\not\exists T, T \not = S \text{ such that } S <: T, m \in m(T) \\}$ The first subset corresponds to a method being directly annotated. The second subset comes into effect if a method in a superclass was annotated. Because of the reflexive property of subtyping , this statement actually subsumes the first rule. The third subset contains the annotations that meet the following three criteria: The method exists in the class or a superclass, the class is annotated with the annotation, and the method had not already been introduced in a class higher up. I defined the semantics of @SuppressSubtypingWarning to act only on the specific method that is annotated with it. If it acquires an annotation in any of the three ways above, but the same method in a superclass does not have the annotation, then the subtyping warning that would normally be generated is suppressed. The @SuppressSubtypingWarning does not have any effect on subtyping warnings that methods in superclasses may generate because they may have annotations that super-superclasses lack.

I also decided to not allow annotations of whole classes because the annotation of a class has effects reaching beyond that class itself: It also affects subclasses. If a class is annotated and a subclass introduces a method, then that method will carry the annotation. Therefore, annotating a class with @SuppressSubtypingWarning would suppress annotations for all methods introduced further down in the hierarchy.