[Checkers] @ReadOnly classes

[Telmo]

Hi,

Mahmood was talking to me the other day about the relation between class 
annotations and method receiver annotations. I finally caught up on the 
problem, when dealing with a test for this purpose: as of now,

@ReadOnly class ReadOnlyEmpty {}

generates an error, (receiver.invalid), because not every method on Object 
has a @ReadOnly receiver. Most likely this change will be added to the 
Javari checker only, unless the IGJ checker also needs it and we decide 
that passing this kind of information from class annotations to method 
receivers is common enough that should be included on the framework.

Namely, what Mahmood proposed, and makes perfect sense, is to add class 
annotations to the receiver types of every method without receiver types.

I am still not clear on the allowances for extensions. If the class A 
extends class B, what are the requirements for subtype relationships?
It seems that A must be a subtype of B, type-wise, so it makes sense to 
restrict that for annotations as well. In order to allow supertype-style 
annotations, such as @ReadOnly, annotations would need to be implictly 
added to every supertype. What is the exact specification, both for Javari 
and the framework, here?

-Telmo