@MustOverride method annotation

Add a @MustOverride method annotation that requires that when a class is subclassed, the method must be overridden. This annotation indicates that the method implementation is broken. It is necessary when the underlying code cannot be fixed, such as when the code is in a library or Java is insufficiently expressive.

An example is:

class ThreadLocal<T> {
  @MustOverride
  T initialValue() { return null; }
}

If a client creates a subclass that does not override initialValue, then get may return null rather than returning T:

new ThreadLocal<Integer>() {
  // BAD: no overrides in this anonymous class declaration
}

Perhaps the method doesn't have to be overridden if the type argument is the top type:

new ThreadLocal<@Nullable Integer>() {
  // OK to have no overrides in this anonymous class declaration
}

Perhaps @MustOverride would take a string argument indicating the reason that the method must be overridden, to help users understand the requirement and when it is acceptable to suppress the warning.

The @MustOverride annotation will solve one problem.
Fully annotating the ThreadLocal class in the JDK requires fixing issue #1330 as well, so that the ThreadLocal constructor can only be invoked with a nullable type:

new ThreadLocal<Integer>();  // Illegal
new ThreadLocal<@Nullable Integer>();  // OK

In the end, ThreadLocal.java will be annotated as:

public class ThreadLocal<@Nullable T extends @Nullable Object> {
  @MustOverride
  T initialValue() { ... }
  ...
}

There is a test case in file checker/tests/nullness/ThreadLocalTest2.java.

Start with the proposed behavior in this issue and the existing test case in checker/tests/nullness/ThreadLocalTest2.java. Review issue #1330 as related work before deciding the scope. Done means the checker supports @MustOverride and the ThreadLocal test demonstrates that required overrides are detected, including the nullable case.