Open davidcok opened 2 years ago
mattulbrich
commented
2 years ago I would drop it from the standard language definition, but support it in tools where appropriate.
This also avoids the difficulty with @NonNull Object[][] not being the same as /@ non_null / Object[][].
leavens
commented
2 years ago I think we should keep support for annotations in JML, as it is very useful. It would also be useful to recognize some standard annotations, such as those form the checker framework and the findbugs tool. Keeping it just for modifiers is fine and seems to cause the least problems.
I'm raising this point just to make sure that we are all in agreement for JMLv2.
Java 5 introduced the @ style annotation to Java, and there was a flurry of work to use these annotations for various tools and meta-processing.
JML tried various things (often student projects). The one that is still around is to use annotations in place of modifiers. That is, instead of
/*@ pure */ public void m()one writes@Pure public void m().This fits in with standard Java and developers are used to using annotations more than specially-formatted comments. Other tools define annotations for their own purpose. There is a
@Nullable, for example, in the checker framework, in the findbugs framework, in javax.annotation etc.The disadvantage is that the Java source code now must include
import org.jmlspecs.annotation.*(so the source code must be changeable), so any other user using the same source code (think a shared GitHub project) must have access to the org.jmlspecs.annotation package, at least for compiling. (I don't think it is needed at runtime).Another aspect of this is that as of Java 11, there are annotations on types -- so the nullable and non_null modifiers need to evolve to being type annotations (rather than declaration annotations) and reasoned about as subtype designators, even if there is no explicit user-facing syntax that uses annotations instead of modifiers.
Also, JML could consider recognizing and using annotations from other systems (particularly the checker framework), at least for nullity, and perhaps for immutability.
The question here is -- should we drop support for Java annotations as synonyms for JML modifiers?
I have no problem with keeping the support, so long as it is just for modifiers (and not full-fledged clauses, for example), but it does complicate the language and implementations.