[CatarinaGamboa]

Closes #514

What and why

With named state sets, a set whose name is also a method name makes state errors read like method calls. With a set named undo, the error says expected undo(undoManager) == undoable, which reads as "the result of undoManager.undo()", the very call that failed. This is a confound for the error-message study.

This PR:

• Adds a warning (not an error: nothing is ambiguous for the verifier) when a @StateSet name is also the name of a method of its class. Inherited methods count too, since x.undo() reads the same either way, except private methods of a superclass. For an @ExternalRefinementsFor spec it checks the methods of the class the spec refines (this includes the methods declared in the spec). Sets without a name are not checked.
• Renames the sets in state_hint_study_undo_manager_correct from phase/undo/redo to phase/undoState/redoState.
• Adds one sentence to the README after the named-set paragraph.

Warning text

Warning: State set name 'undo' is also the name of a method of UndoManager, so undo(x) == undoable reads like a call to undo(). Choose another name, such as undoState

The example state is the first state of the set.

Before / after (real verifier output)

state_hint_study_undo_manager_error from main, with its sets named as in the correct fixture. Only the UNDO error is shown; REDO is the same.

Before (main, sets phase/undo/redo): no warning, and the error reads like a call.

State Refinement Error: expected undo(undoManager) == undoable but could not prove it
33 |             case UNDO -> undoManager.undo(); // Expect: State Refinement Error
   |                          ^^^^^^^^^^^^^^^^^^^

After (this branch, same names): two warnings on the set names, then the same errors.

Warning: State set name 'undo' is also the name of a method of UndoManager, so undo(x) == undoable reads like a call to undo(). Choose another name, such as undoState
20 | @StateSet(name="undo", value={"undoable", "notUndoable"})
   |                 ^^^^

Warning: State set name 'redo' is also the name of a method of UndoManager, so redo(x) == redoable reads like a call to redo(). Choose another name, such as redoState
21 | @StateSet(name="redo", value={"redoable", "notRedoable"})
   |                 ^^^^

After renaming to phase/undoState/redoState: no warning, and the error no longer looks like a call.

State Refinement Error: expected undoState(undoManager) == undoable but could not prove it
33 |             case UNDO -> undoManager.undo(); // Expect: State Refinement Error
   |                          ^^^^^^^^^^^^^^^^^^^

Tests

Three // Expect: Warning cases and one no-warning case added to the existing ErrorStateSetNames fixture. Each one fails without the fix (main reports 6 diagnostics on the file, the fixture expects 9):

• ErrorStateSetNameOfAMethod: a set undo on a class with a method undo().
• ErrorStateSetNameOfAnInheritedMethod: a set undo on a subclass that inherits undo(). It also has a set reset with no expected warning, because the superclass's reset() is private (without that rule it warns once too many).
• ErrorStateSetNameOfAMethodOfTheTarget: an @ExternalRefinementsFor("java.util.ArrayList") spec with a set clear.

The renamed undo manager fixture keeps passing with no warning. Full mvn test passes locally.

🤖 Generated with Claude Code

[CatarinaGamboa]

Clean-code review

Audit of this PR's own new code only (warnIfStateSetNameIsAMethod in TypeChecker, the fixture cases, the README sentence), with the clean-code-principles checklist.

• TypeChecker.java warnIfStateSetNameIsAMethod - [core-kiss / readability] One if mixed three unrelated reasons to skip (a set without a name, an unknown type, no clashing method). Fixed (in the next push): the "set without a name" case is its own early return with a short comment saying why, before the type lookup.
• Same method - [solid-srp] It both finds the clash and reports it. Declined: it mirrors the neighbouring checkStateSetNameIsFree, which does the same, and splitting a 10-line method would not make it clearer.
• Same method - [pattern / org] A dedicated LJWarning subclass (like UnsatisfiableRefinementWarning) instead of CustomWarning. Declined: nothing reads the warning's fields (no IDE quick fix uses them), and the PM's rule is not to add classes for tidiness.
• Same method - [core-dry] The format string passes name four times. Declined: positional %s arguments match the rest of the file; %1$s would be harder to read for a one-off message.
• Same method - orElse("...") fallback for a set with no states. Declined as a finding: it only guards an empty @StateSet({}), which is legal; the message stays readable.
• Fixtures / README: no findings. The fixture comment cites Warn when a state set is named like a method of its class #514 (allowed in fixtures); no issue numbers under liquidjava-verifier/src/main.

[CatarinaGamboa]

Codex

• False warning for methods that are not inherited (TypeChecker.java). getAllMethods() includes methods declared on ancestors even when the target cannot inherit them. For example, class Parent { private void reset() {} } and @StateSet(name="reset", value={"ready"}) class Child extends Parent {} produces a warning, although Child has no reset() method. A package-private ancestor method across package boundaries has the same problem. This also affects external specs targeting Child. The existing inheritedMethods filter in ExternalRefinementTypeChecker shows the relevant visibility rules.

• Test gap: The new examples cover a declared method, an inherited method, and an external target, but none covers an inaccessible ancestor method. The example harness also checks warning count and line only, so it cannot catch an incorrect warning message.

Skipping unnamed sets matches the stated intent. I did not run mvn install or other tests.

[CatarinaGamboa]

Codex round 1: fixed / declined

Pushed with the clean-code fix. Full mvn test passes locally.

• Private method of a superclass counted as a method of the class: fixed. A method counts when it is declared on the class itself (any visibility, since the class can call its own private methods) or is not private. ErrorStateSetNameOfAnInheritedMethod now also has a set reset where the superclass's reset() is private, with no expected warning; it fails without the fix (4 warnings instead of 3).
• Package-private superclass method across packages: declined. It needs a superclass in another package that declares a package-private method with the same name as the set; the cost of a wrong warning there is one suggestion to rename. Copying the package walk from ExternalRefinementTypeChecker.inheritedMethods would double the size of the change.
• The harness does not check the warning text: declined. That holds for every warning in the suite; the real text is in the PR body.

[CatarinaGamboa]

Codex

Finding: The inherited-method check can warn on a method that the annotated interface does not inherit. Spoon’s getAllMethods() includes methods declared by parent interfaces, and the filter excludes private methods but not static interface methods (TypeChecker.java).

Concrete input:

interface Parent {
    static void reset() {}
}

@StateSet(name = "reset", value = {"fresh", "used"})
interface Child extends Parent {}

Child has no callable reset() method, but this check emits the warning. The same case applies when an external spec targets Child. Exclude static methods declared on parent interfaces.

Test gap: The new external-spec test covers a method declared directly on ArrayList, but not one inherited by the target. A spec targeting an ArrayList subclass with a set named clear would exercise that path.

I did not run tests or mvn install.

[CatarinaGamboa]

Codex round 2: fixed / declined

Nothing changed in this round, so no push.

• Static method of a parent interface counted for a sub-interface: declined. It needs a state set on an interface whose parent interface declares a static method with the same name as the set. A wrong warning there costs one rename suggestion, and handling it would add another clause and another fixture case for a case no spec uses.
• External spec whose target inherits the clashing method: declined. The check calls the same getAllMethods() on the target type for both classes and external specs, so ErrorStateSetNameOfAnInheritedMethod already covers the inheritance path; another fixture would not fail for a different reason.

Codex's remaining findings are edge cases already declined, so the loop stops here (2 rounds).