[CatarinaGamboa]

Fixes #494

The verifier had no switch handling, so the cases ran one after another as straight-line code: break was ignored and the case label never entered the path condition. A switch is now checked like the if / else if chain over its labels:

• each case starts from the state before the switch and knows selector == label (grouped labels: any of them; default: none of the other labels)
• a case without break falls through into the next one
• the states of the cases that reach the end are joined after the switch, as after an if
• return / throw / continue in a case drop that path, as in an if
• switch expressions (->, yield) are checked the same way; selectors may be enums, ints or strings (a string label has no known value, so it adds no path condition)

Two forms are handled conservatively:

• pattern or guarded cases (case String s ->, when): checked as before (Verifier crashes on a type-pattern switch (case String s ->) #345 is unchanged)
• a break / yield nested inside a case (e.g. if (c) { ...; break; }): the state at that jump is not followed, so what those cases change is forgotten on that path after the switch (shown as true in Found)

Study exercise A1_09 (litiengine), the partial fix else if (newMode == BORDERLESS) host.dispose();

Before, the same error at the same line, though BORDERLESS is now disposed:

State Refinement Error: found previousMode == BORDERLESS && newMode != BORDERLESS ? notDisplayable(host) : (newMode == BORDERLESS ? notDisplayable(host) : displayable(host)) but expected notDisplayable(host)
49 |         host.setUndecorated(true);

After, the error moves to the remaining bug, the full-screen fallback:

State Refinement Error: found newMode == FULLSCREEN && (previousMode == BORDERLESS && newMode != BORDERLESS ? notDisplayable(host) : (newMode == BORDERLESS ? notDisplayable(host) : displayable(host))) but expected notDisplayable(host)
62 |           host.setUndecorated(true);

Study exercise A1_56 (JabRef), only redo() guarded

Before, the UNDO case saw what the REDO case did:

State Refinement Error: found (#canRedo_result ? redoable(undoManager@70) : notRedoable(undoManager@70)) && state2(undoManager@70) == state2(#getUndoManager_result) && limit(undoManager@70) == limit(#getUndoManager_result) && (#canRedo_result ? undoable(undoManager) && notRedoable(undoManager) && ... : ...) but expected undoable(undoManager)

After, only what holds on the UNDO path:

State Refinement Error: expected undoable(undoManager) but could not prove it
72 |                     case UNDO -> undoManager.undo();
Hints:
  - The state of undoManager is unknown here, and this call needs it to be undoable
  - Guard this call with if (undoManager.canUndo()): when it returns true, undoManager is undoable

The six study exercises still report their error at the same line. A1_09's Found now starts with the case's label: found newMode == BORDERLESS && (...). The other study variants report the same as before, apart from A1_09's first-only fix: same line (63), but its Found was displayable(host), the state the BORDERLESS case left, and is now the full-screen path's newMode == FULLSCREEN && (...), longer than before.

Tests: CorrectEnumUsage (state and label of each case, switch statement and expression), ErrorEnumUsage (an error that was missed in a case reached directly and by fall-through, and the nested break). TestStateHints now expects A1_56's UNDO hints above. Each fails on main.

🤖 Generated with Claude Code

[CatarinaGamboa]

Codex review, round 1

[P2] Exclude the unmatched path for exhaustive enum switches (RefinementTypeChecker.java:671-672). When a switch covers every constant of an enum but has no default, this branch still treats "no label matches" as a path that reaches the code after the switch. For example, if every case moves an object to the same required typestate, the join also includes its pre-switch state and can incorrectly reject a valid call afterward. Detect exhaustive enum switches before adding the unmatched path.

[CatarinaGamboa]

Round 1 replies:

• Exhaustive enum switches: partly fixed, partly declined.
  • Declined for enums declared in the analyzed sources. Their constants are values of an SMT enum sort, so when every constant has a case, "no label matches" is already unsatisfiable. I checked: a switch statement with case RED / GREEN / BLUE that each close(), followed by reopen(), verifies.
  • Declined for switch statements over library enums. A switch statement with no default really can match no label: Java adds no default, so a constant added to the enum later reaches the code after it.
  • Fixed for switch expressions, which Java makes exhaustive: when no label matches, the code it adds throws. That path no longer reaches the code after the switch. Covered by CorrectEnumUsage.captureOnThread, on Thread.State, a library enum whose labels the verifier cannot translate. That test fails without the change.

[CatarinaGamboa]

Codex review, round 2: no findings ("I found no actionable regressions in the diff. The verifier test suite passed.").

[CatarinaGamboa]

Clean-code review (clean-code-principles)

Reviewed the diff only, weighed against the standing rules (smallest PR that tests well, match surrounding style, no tidy-only refactors, lean tests). Nothing worth a commit and CI run; no new commits.

Finding	Verdict
RefinementTypeChecker.java visitCases - [core-dry] repeats the if-modelling sequence of visitCtIf (variablesNewIfCombination / SetBeforeIf / then / else / keep-the-only-reaching-guard / CombineFromIf)	Declined. Sharing it would mean refactoring visitCtIf, which is existing code. The Javadoc already says the switch is checked "as the chain of ifs", so a reader can follow the parallel.
RefinementTypeChecker.java visitCases - [func-few-arguments] 7 parameters	Declined. Most of them are recursion state. Bundling them needs a new holder type, which adds more than it removes for one private recursive method.
RefinementTypeChecker.java visitSwitch - [solid-srp-function] it both scans labels and groups cases into CaseEntrys	Declined. The grouping scans each label as it goes, so splitting it out would separate the side effect from the loop that orders it. At about 40 lines with a comment per stage, the method reads fine.
RefinementTypeChecker.java visitCasesFrom - [core-kiss-readability] c.getStatements() is read for the loop, then read again into statements two lines later	Declined. It is purely cosmetic and not worth a CI run. Worth folding in if the PR is touched again.
changedIn(CtLoop) -> changedIn(element, scope), removeCheckMetadata(loop) -> (element, checkedBefore) - [core-dry]	OK. These reuse existing code by generalizing it, with no copy and no new class.
GeneratedNames.SWITCH_SELECTOR / CASE_CONDITION - [name-searchable]	OK. They follow the existing IF_CONDITION / TERNARY_CONDITION constants.
Comments - [doc-why-not-what]	OK. The new comments explain reasons, for example that the selector is evaluated once, why a case is re-checked after a fall-through, and why a switch expression without a default does not reach the end.
Tests - [lean tests] fixture methods in CorrectEnumUsage / ErrorEnumUsage and one updated TestStateHints expectation	OK. Each fixture method covers a distinct rule (statement switch, expression switch, exhaustive expression, fall-through, break inside an if).