State hints: name only the state the call leads to, and no guard when a call sequence works by CatarinaGamboa · Pull Request #524 · liquid-java/liquidjava

CatarinaGamboa · 2026-11-10T15:06:04Z

Closes #518
Closes #519

What and why

Changes to the state hints in StateHints (display and choice of hints only; the VC, verdict and category are unchanged):

Call sequences name only the state they lead to (State hints: name only the state the call leads to #519): Call S before this call; afterwards <state>. The "from" part is gone, since the Found already shows it. In A1_09 it listed every state of the set (from display(host) == notDisplayable or display(host) == displayable). "Afterwards" is the machine's after state for the changed sets, so the hint only states what the machine computes after the calls, and no != is turned into ==. The value form from Show states of named sets by their set in state hints and declared-here #517 stays (markState(buffered) == marked). Classes with no named set read afterwards f is open.
A deciding argument is written as the call (State hints: name only the state the call leads to #519): when a step's condition is param == c for the method's only parameter, and c names no variable, the step is written wParam.setCompressionMode(ImageWriteParam.MODE_EXPLICIT). Any other condition keeps r.set(int lo, int hi) with lo < hi.
No GUARD hint when a CALL_SEQUENCE hint exists (Drop the guard hint when a call-sequence hint exists, and reword it #518). Wrapping the call in the check skips it in exactly the failing case. In A1_09 the verifier accepts that fix and the study grader marks it INCORRECT. Before, the guard was dropped only for a single known state. The unknown-state hints (A1_56) do not change: its guard stays, since it has no call sequence and the guard is the reference fix.
Guard wording (Drop the guard hint when a call-sequence hint exists, and reword it #518): Guard this call with if (<check>); inside it, <state>. This replaces "when it returns false", which was ambiguous next to !host.isDisplayable().
AVAILABLE_CALLS ("can call") is dropped when any other hint is given (State hints: name only the state the call leads to #519). FINAL_STATE is unchanged.

Study tasks (CLI, before = main, after = this branch)

Each task still gives exactly one error, on its reportedLine. A2_10, A2_04, practice and practice2 are unchanged.

A1_38

before:
  - Call buffered.mark(int) before this call to move buffered from markState(buffered) == unmarked to markState(buffered) == marked
  - When stream(buffered) == open and markState(buffered) == unmarked, buffered can call: read(), read(byte[], int, int), skip(long), available(), mark(int), ...
after:
  - Call buffered.mark(int) before this call; afterwards markState(buffered) == marked

A1_01

before:
  - Call wParam.setCompressionMode(int mode) with mode == ImageWriteParam.MODE_EXPLICIT before this call to move wParam from compression(wParam) == compressionNotExplicit to compression(wParam) == compressionExplicit
  - When tiling(wParam) == tilingNotExplicit and compression(wParam) == compressionNotExplicit, wParam can call: setTilingMode(int), setCompressionMode(int) (and possibly others)
after:
  - Call wParam.setCompressionMode(ImageWriteParam.MODE_EXPLICIT) before this call; afterwards compression(wParam) == compressionExplicit

A1_09

before:
  - Call host.dispose() before this call to move host from display(host) == notDisplayable or display(host) == displayable to display(host) == notDisplayable
  - Call host.removeNotify() before this call to move host from display(host) == notDisplayable or display(host) == displayable to display(host) == notDisplayable
  - Guard this call with if (!host.isDisplayable()): when it returns false, display(host) == notDisplayable
  - When display(host) == notDisplayable or display(host) == displayable, host can call: pack(), dispose(), addNotify(), removeNotify() (and possibly others)
after:
  - Call host.dispose() before this call; afterwards display(host) == notDisplayable
  - Call host.removeNotify() before this call; afterwards display(host) == notDisplayable

host.dispose() is still the first hint. analysis/check-fixes.py --selftest --task A1_09 passes 8/8 and grades the plain dispose() fix (P01) CORRECT.

A1_56 (the guard stays)

before:
  - The state of undoManager is unknown here, and this call needs redoState(undoManager) == redoable
  - Guard this call with if (undoManager.canRedo()): when it returns true, redoState(undoManager) == redoable
after:
  - The state of undoManager is unknown here, and this call needs redoState(undoManager) == redoable
  - Guard this call with if (undoManager.canRedo()); inside it, redoState(undoManager) == redoable

IDE

Hints reach vscode-liquidjava as plain message text, so they show there with no extension change. There are no screenshots, because nothing in the extension's layout changes.

Tests

The exact-message expectations in TestStateHints are updated. Each of these fails on main: the new wording, no "can call" next to another hint, and setCompressionMode(2) / chain.pick(1) for the argument form. One case is added to the existing ErrorStateHintGuards fixture: reachableOnEveryPath, the A1_09 shape (path-dependent state, a call that reaches the needed state, a query). On main it gives a sequence, a guard and "can call"; now it gives only the sequence. The full suite passes locally (728 tests).

Open for the PM

The unknown-state hints (anyState, used by A1_56) can also list a call sequence after the guard. Drop the guard hint when a call-sequence hint exists, and reword it #518 scopes the rule to forCall, so the guard is kept there. None of the study tasks has both.

🤖 Generated with Claude Code

… a call sequence works - A call-sequence hint now reads "Call S before this call; afterwards <state>", with no "from" part: the state before is in the message. - A step whose condition gives its only parameter a value is written as the call with that value, e.g. wParam.setCompressionMode(ImageWriteParam.MODE_EXPLICIT). - No guard hint when a sequence of calls reaches a state that allows the call: wrapping the call in the check would skip it where it fails. - The guard reads "Guard this call with if (<check>); inside it, <state>". - The calls allowed now are listed only when no other hint is given. Closes #518 Closes #519 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

CatarinaGamboa · 2026-11-10T15:06:16Z

Clean-code review

I audited this PR's new code only (clean-code-principles). The PM's small-PR rule takes precedence.

Fixed

StateHints.allowedCalls: [func-few-arguments / flag argument] my first version added a boolean onlyHint parameter. Now forCall filters out AVAILABLE_CALLS itself, and allowedCalls keeps its old signature.
StateHints.callSequence / howToReach: [core-yagni] fromAnyState existed only to print "from any state". It is removed along with the "from" part.
StateHints.guard / callSequence: [core-dry] both built (asValues ? "" : receiver + " is ") + states. They now share isIn.

Declined

StateHints.call(CallVariant): [core-dry] receiver + "." + simpleName + "(" ... ")" is close to guardCall. Declined: they differ in what goes in the parentheses, and a shared helper would save one line.
argumentValue: [core-kiss] it handles only a method with one parameter. Declined: for several parameters it would have to write the others as ..., which the issue does not ask for. Those keep the with <condition> form, which is sound.

There are no SOLID or layering issues. All the wording stays in StateHints.

CatarinaGamboa · 2026-11-10T15:16:31Z

Codex review, round 1

No findings. Codex reran TestStateHints and every state-hint fixture through the CLI and found no actionable regression. The review loop ends here.

The full suite passes locally (728 tests).

…fer to (#533) Closes #532. **Stacked on #530** (→ #528 → `main`). Retarget it to `main` before #530 is merged with `--delete-branch`. Every message that shows code now marks it with backticks, inside the message string: - headlines (`found … but expected …`, `expected … but could not prove it`); - hints; - origin notes; - the declared-here gloss (`where … means …`); - alias `where` lines; - counterexamples. ## How each client sees it - **Plain text** (`getMessage()`, `getMessageNotes()`, `Hint.message()`, `getCounterexampleStr()`, `getDeclarationNotes()`, and so the Problems tab and the hover): the string with backticks, as rustc writes its messages. - **CLI:** each span in blue (the existing `Colors.BLUE`), without backticks. The backticks stay when colour is off: `NO_COLOR` set (https://no-color.org) or no console (output piped or redirected). The colour switch applies to code spans only; the CLI's other colours are unchanged. - **IDE:** the same backticked strings, plus `LJDiagnostic.getReferences()`, a `List<SourceReference>` with one entry per line reference. See below. **Escaping:** `Code.of` fences code that holds backticks with a longer run, and pads it with one space on each side when it holds a backtick or starts or ends with a space: ``` `` c == '`' `` ```. `Code.render` strips exactly that padding, so it shows any non-empty code exactly as marked. ## Source references (for vscode-liquidjava#192) `record SourceReference(String message, String text, int start, String file, int line, int column)`: - `message`: the whole message line it belongs to, exactly as `getMessageNotes()` or `Hint.message()` gives it; - `text`: the words of `message` that name the place, e.g. `line 134` or `ArrayListRefinements.java:162`; - `start`: where `text` starts in `message`, as a UTF-16 index (a Java/JS string index), so `message.substring(start, start + text.length())` is `text`. Use it instead of searching, because the code of a call can hold the same words (`d.lock("line 18")` on line 18); - `file`: the absolute path; `line`, `column`: 1-based, from Spoon. Who carries one: - every origin note: the call, parameter, constructor or return-refinement declaration it names; - the deciding-argument hint (`… on line 20 decides …`), through the new `Hint.reference()`, which is null for other hints. `getReferences()` returns the notes' references first, then the hints'. ## Before → after (CLI piped, so backticks shown) ```text A1_38 State Refinement Error: found `stream(buffered) == open && markState(buffered) == unmarked` but expected `markState(buffered) == marked && stream(buffered) == open` Origin: line 134, `new BufferedInputStream(stream)` makes `markState(buffered) == unmarked` - Call `buffered.mark(int)` before this call; afterwards `markState(buffered) == marked` where `marked(this)` means `markState(this) == marked`, `open(this)` means `stream(this) == open` A1_01 Origin: line 130, `writer.getDefaultWriteParam()` returns `compression(wParam) == compressionNotExplicit` - Call `wParam.setCompressionMode(ImageWriteParam.MODE_EXPLICIT)` before this call; afterwards `compression(wParam) == compressionExplicit` A2_04 Refinement Error: expected `timeout >= 0` but could not prove it Origin: line 94, `timeout` is a parameter of `checkCimReachable(String, int)` with no refinement --> Counterexample: `timeout == -1` A1_56 Origin: line 69, `frame.getUndoManager()` says nothing about `redoState(undoManager)` - Guard this call with `if (undoManager.canRedo())`; inside it, `redoState(undoManager) == redoable` A2_10 Refinement Error: found `failures.size() == size(this.failures) && failures.size() >= 0` but expected `failures.size() > 0` Origin: ArrayListRefinements.java:162, `failures.size()` guarantees only `failures.size() >= 0` ``` For all eight tasks (six study tasks and both practice tasks), the output with backticks removed is byte-identical to #530's. Each task still gives exactly one error, on its `reportedLine`. On a terminal the spans are blue and the backticks are gone. With `NO_COLOR=1` the backticks stay. ## Changes - `Code` (`of`, `render`), `SourceReference`, and `Colors.enabled()`. - `LJDiagnostic`: - `addMessageNote(SourceReference)` and `getReferences()`; - `toString` renders the message, notes, counterexample, hints and declaration notes. - Marked at the leaves where messages are built: - `ErrorMessage` (both headline frames); - `RefinementError` (counterexample, alias lines); - `AuxStateHandler.addMeanings` (gloss); - `StateHints`: each state name, call, receiver and constructor, with the prose words `or`, `and`, `then`, `with` left unmarked; - `OriginNotes`/`StateOrigin`, whose notes are now `SourceReference`s. - `NotFoundError` marks the missing name and the suggestion (``Alias `Positiv` could not be found``, ``Did you mean `Positive`?``). - Not marked: the other error kinds (state conflicts, syntax errors) and warnings, which the issue does not list. They are a follow-up if wanted. ## Tests - 59 existing expectations gained backticks. Each change was made by a script that accepts a new string only if removing its backticks gives exactly the old one. - `TestStateHints.assertHints` compares kind and message. - New tests, each failing without the change: - `CodeTest` (fence, colour on and off); - `TestOriginNotes.noteNamesTheLineOfTheCallForClientsToLinkTo`; - a reference check in the deciding-argument hint test. `mvn test`: 740 run, 0 failures. ## Conflicts - **#524 and #525 are merged**, and this branch sits on top of them (via #528's rebase), so it does not conflict with them. The lines of their code it changes are: - `StateHints.java`, on main: the hint templates at 116–119, 131–132, 182–184, 234, 239–240, 249, 252, 258, 260, 269, 295–297, 301, 303–305, 349, and `stateName` at 387–389; - `RefinementError.java`, on main: 71 (counterexample) and 123 (alias `where` lines); - `ErrorMessage.java` 39–41 (headline); - `AuxStateHandler.java` 865–866 (gloss). - With the #529 agent's work: both may touch `VCChecker.throwStateRefinementError`. This PR changes only the notes' parameter type there. 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>

CatarinaGamboa merged commit c4c6ce1 into main Nov 10, 2026
1 check passed

This was referenced Nov 10, 2026

Origin note: say where the wrong state of a receiver comes from #528

Merged

Mark code in every message with backticks, and name the lines they refer to #533

Merged

Navigation Menu

Repository navigation

State hints: name only the state the call leads to, and no guard when a call sequence works - #524

State hints: name only the state the call leads to, and no guard when a call sequence works#524
CatarinaGamboa merged 1 commit into
mainfrom
state-hints-518-519

CatarinaGamboa commented Nov 10, 2026

Uh oh!

CatarinaGamboa commented Nov 10, 2026

Uh oh!

CatarinaGamboa commented Nov 10, 2026

Uh oh!

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

CatarinaGamboa commented Nov 10, 2026

What and why

Study tasks (CLI, before = main, after = this branch)

IDE

Tests

Open for the PM

Uh oh!

CatarinaGamboa commented Nov 10, 2026

Clean-code review

Uh oh!

CatarinaGamboa commented Nov 10, 2026

Codex review, round 1

Uh oh!

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant