Warn when a state set is named like a method of its class

README.md

@@ -67,6 +67,8 @@ A state set can be given a `name`, and a state is then written as a value of its
 State Refinement Error: found connection(socket) == bound but expected connection(socket) == connected
 ```
 
+Choose set names that are not also names of methods of the class: with a set named `undo`, `undo(x) == undoable` reads like a call to `undo()`, so LiquidJava warns about such names.
+
 Lambda bodies are checked separately from the code that creates them. Creating a lambda does not apply its state
 transitions to captured objects. While checking the body, LiquidJava keeps declared refinements but forgets the current
 state of mutable captures, since that state may change before invocation. Callback execution summaries are not supported:

liquidjava-example/src/main/java/testSuite/ErrorStateSetNames.java

@@ -1,11 +1,13 @@
 package testSuite;
 
+import liquidjava.specification.ExternalRefinementsFor;
 import liquidjava.specification.Ghost;
 import liquidjava.specification.RefinementPredicate;
 import liquidjava.specification.StateSet;
 
 // A state set name must be a lowercase identifier that no state, ghost or other state set of the class uses, and
-// not one of the names given to state sets without a name
+// not one of the names given to state sets without a name. A name that is also a method of the class is only a
+// warning (#514): undo(x) == undoable reads like a call to undo()
 @StateSet(name = "Door", value = {"closed", "opened"}) // Expect: Error
 public class ErrorStateSetNames {}
 
@@ -27,3 +29,17 @@ class ErrorStateSetNameOfARefinementPredicate {}
 
 @StateSet(name = "state2", value = {"closed", "opened"}) // Expect: Error
 class ErrorStateSetNameOfAGeneratedName {}
+
+@StateSet(name = "undo", value = {"undoable", "notUndoable"}) // Expect: Warning
+class ErrorStateSetNameOfAMethod {
+    void undo() {}
+    private void reset() {}
+}
+
+@StateSet(name = "undo", value = {"undoable", "notUndoable"}) // Expect: Warning
+@StateSet(name = "reset", value = {"fresh", "used"}) // no warning: reset() is private to the superclass
+class ErrorStateSetNameOfAnInheritedMethod extends ErrorStateSetNameOfAMethod {}
+
+@ExternalRefinementsFor("java.util.ArrayList")
+@StateSet(name = "clear", value = {"empty", "nonEmpty"}) // Expect: Warning
+interface ErrorStateSetNameOfAMethodOfTheTarget {}

liquidjava-example/src/main/java/testSuite/classes/state_hint_study_undo_manager_correct/UndoManagerRefinementsExpert.java

@@ -17,8 +17,8 @@
 // once (AbstractUndoableEdit.hasBeenDone), so end() makes it undoable and not redoable.
 @ExternalRefinementsFor("javax.swing.undo.UndoManager")
 @StateSet(name="phase", value={"start", "canEdit", "end"})
-@StateSet(name="undo", value={"undoable", "notUndoable"})
-@StateSet(name="redo", value={"redoable", "notRedoable"})
+@StateSet(name="undoState", value={"undoable", "notUndoable"})
+@StateSet(name="redoState", value={"redoable", "notRedoable"})
 public interface UndoManagerRefinementsExpert {
 
     @StateRefinement(to="start(this) && notUndoable(this) && notRedoable(this)")
@@ -81,9 +81,9 @@ public interface UndoManagerRefinementsExpert {
     // Queries: they never change the manager, they tell the verifier which state it is in. When it is
     // already known to be undoable / redoable the answer is true; otherwise (not known, or a field whose
     // state is unknown) the answer decides.
-    // When canUndo() returns false it keeps the undo set by name.
+    // When canUndo() returns false it keeps the undoState set by name.
     @StateRefinement(from="undoable(this)", to="return && undoable(this)")
-    @StateRefinement(to="return ? undoable(this) : undo(this) == undo(old(this))")
+    @StateRefinement(to="return ? undoable(this) : undoState(this) == undoState(old(this))")
     boolean canUndo();
 
     @StateRefinement(from="redoable(this)", to="return && redoable(this)")

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java

@@ -12,6 +12,7 @@
 import liquidjava.diagnostics.errors.*;
 import liquidjava.diagnostics.categories.ErrorCategory;
 import liquidjava.diagnostics.hints.Hint;
+import liquidjava.diagnostics.warnings.CustomWarning;
 import liquidjava.diagnostics.warnings.UnsatisfiableRefinementWarning;
 import liquidjava.processor.context.AliasWrapper;
 import liquidjava.processor.context.Context;
@@ -230,8 +231,10 @@ public void registerGhostsAndStateSets(CtElement element) throws LJError {
         }
         // checked once every set and ghost of the class exists, so the order of the annotations does not matter; a
         // generated name such as state1 can clash too
-        for (Map.Entry<GhostFunction, SourcePosition> stateSet : stateSets.entrySet())
+        for (Map.Entry<GhostFunction, SourcePosition> stateSet : stateSets.entrySet()) {
             checkStateSetNameIsFree(stateSet.getKey(), stateSet.getValue());
+            warnIfStateSetNameIsAMethod(stateSet.getKey(), stateSet.getValue());
+        }
     }
 
     /**
@@ -285,6 +288,28 @@ private void checkStateSetNameIsFree(GhostFunction set, SourcePosition position)
                     set.getParentClassName()), position);
     }
 
+    /**
+     * Warns about a named state set whose name is also the name of a method of its class, or of the class an external
+     * spec refines: in a message such as {@code undo(x) == undoable} the set reads like a call to that method
+     */
+    private void warnIfStateSetNameIsAMethod(GhostFunction set, SourcePosition position) {
+        String name = set.getName();
+        if (name.matches(Formats.STATE_SET_NAMES))
+            return; // a set without a name, whose name the user did not choose
+        CtType<?> type = factory.Type().createReference(set.getPrefix()).getTypeDeclaration();
+        // a private method of a superclass is not a method of this class
+        if (type == null || type.getAllMethods().stream()
+                .noneMatch(m -> m.getSimpleName().equals(name) && (m.getDeclaringType() == type || !m.isPrivate())))
+            return;
+        String state = context.getGhostState(set.getParentClassName()).stream().filter(gs -> gs.getParent() == set)
+                .map(GhostState::getName).findFirst().orElse("...");
+        diagnostics.add(new CustomWarning(position,
+                String.format(
+                        "State set name '%s' is also the name of a method of %s, so %s(x) == %s reads like a "
+                                + "call to %s(). Choose another name, such as %sState",
+                        name, set.getParentClassName(), name, state, name, name)));
+    }
+
     private GhostFunction createStateSet(CtNewArray<String> e, String name, CtElement element) throws LJError {
 
         // if any of the states starts with uppercase, throw error (reserved for alias)