Any hope of cleaning up the annotation names in GUI Effect?

[Jo D]

I'm finding it incredibly hard to build an intuition for the GUI Effect checker.

I believe one of the causes is terminological: I'd expect that e.g. @UI is some sort of umbrella, but actually it's a type annotation for the polymorphic case.

So... is there any hope to clean this up?

Things to consider:

• Unify letter case and spelling.
  Sometimes it's "uieffect", sometimes "GUIEffect", sometimes "GuiEffect".
  Any such difference makes the reader wonder whether the difference is just an inconsistency, or supposed to convey some subtle difference.
  (Of course, inconsistencies due to Java conventions should not be eliminated - if it's a package name, it shouldn't have uppercase letters, etc.)
• Do not have separate names for member annotations and class/package annotations. Just reuse the member annotations for the class/package case if they're just defining a default.
• "Effect" is a pretty inscrutable terminology - in programming, the term is so overloaded it's almost guaranteed to evoke the wrong understanding.
  I'd rather say @GuiThread (may access GUI-thread data) or @GuiAgnostic (does not access GUI-thread data so it may be accessed/called from inside or from outside the GUI thread).
• With the above suggestions, we get just two annotations to remember and a simple rule about when it's a specification (on member variables and functions) and when it's just a default (on classes and packages).
  Old-to-new annotation mappings would be:
  • @SafeEffect, @SafeType -> @GuiAgnostic
  • @UIEffect, @UIType, @UIPackage -> @GuiThread
  • @PolyUIEffect, @PolyUIType -> @GuiPolymorphic (but see next bullet point)
• The @PolyUI annotation family was utterly confusing to me because the naming scheme for the instantiations is actually misleading:
  • @AlwaysSafe, @UI, @PolyUI (Instantiation)
  • @PolyUIEffect, @PolyUIType (Declaration)

Note that the suggested names all start with @Gui, so it's easy to have an IDE search for them; such properties are irrelevant for the theory but very relevant when working with them.

I also have two semantic suggestions:

• New annotation: @GuiBanned.
  To declare that a member function must not ever access anything @GuiThread.
  SwingWorker#doInBackground would be a candidate, and pretty important for us because we use it extensively (FWIW).
  (Or maybe I overlooked to do declare "must not access @GuiThread stuff"?)
• Make @GuiThread, @GuiAgnostic, and @GuiBanned annotations on member functions be inheritable.
  If a parent class declares something @GuiThread, it makes no sense to ask a subclass to repeat the annotation on every single member function.
  This is a real pain for our project, because we have tons of classes that inherit from Swing classes and override tons of stuff; I cannot imagine how a restriction on the superclass member cannot apply to any overriding subclass member. (Well, you could do some design-by-contract-style relaxations - the subclass might redefine a member to do nothing, in which case it could be redeclared as @GuiAgnostic. But that kind of stuff is such a rare exception that even in our 180 kLoC I have seen less than half a dozen instances of this, and I highly suspect that all cases are ill-advised anyway, all Swing code is there for a reason but ah well the legacy...)
  New class members would pick up their @Gui status from whatever is the default for the class, because they don't override anything.

I know that the changes suggested above could be disruptive, so I'm prepared to see them shot down instantly.

Also, I'm pretty new to Checker Framework, so I might be blatantly off course with some ideas. Please be gentle :-)

Regards,

Jo