[CatarinaGamboa]

Part of #502 (PR 1, the language). Depends on #507 and #508. Until they are merged, this diff also shows their commits; only the last commit belongs here.

What

A spec can write a state as a value of its set:

@StateSet(name = "door", value = {"closed", "opened"})
@StateSet(name = "lock", value = {"unlocked", "locked"})
...
@StateRefinement(from = "door(this) == closed && lock(this) != locked", to = "door(this) == opened")
void open();

set(e) == state means state(e), and set(e) != state means !state(e), in either order. The old shorthand stays valid, and the two can be mixed.

How

StateValues.toShorthand rewrites the new form into the shorthand once, where the spec is parsed and in that spec's scope. Everything after that is unchanged, and that includes every part that reads states syntactically: the frame equalities, the state machine, the hints, DecidingArgument, StateErrorCategories and #495's relevance pass. The parse sites are:

• @Refinement, via getRefinementFromAnnotation;
• method from/to, via createStatePredicate;
• constructor to, via setConstructorStates;
• alias bodies, at registration, where only the alias's parameters are variables.

Every set is already registered when specs are parsed (#508), so there is no late resolution, and a caller's variable can never capture a state name.

Scope rules (from the #502 design reviews):

• A variable in scope keeps its meaning. That covers parameters, context variables, and _, this and return, which are always variables. Specs that are valid today mean the same.
• A name that is a state of another set of the class is an error: State 'locked' is not a state of 'door' (its states are closed, opened).
• Only the sets that apply to the argument's type are considered, that is, sets declared on its class or a supertype. The type comes from this, _, a parameter, a context variable, old(x), or an alias's declared parameter type. When the type is known, any applicable set may have the state, as with the shorthand. When it is unknown, every set of that name must have it, and otherwise the name stays an unknown variable. The rewritten state is named exactly as the shorthand written in the same place (a.Sub.door(this) == open becomes a.Sub.open(this)), so it is resolved the same way.

Two new checks on @StateSet (⚠️ breaking for specs that have this ambiguity today: they are now rejected even if the ambiguous state is never used), because open(this) must say which set it means:

• Two sets of one class may not share a state name: State 'open' is in two state sets of X: state1 and state2. That was accepted before, and the shorthand picked one set silently.
• The Named state sets: optional name on @StateSet #498 name check now covers generated names, so a state called state1 next to the unnamed set state1 is reported.

Tests (each fails without the change)

• CorrectStateValues, written only in the new form: two named sets, a constructor to, from/to, !=, a branch that keeps a set via old, a parameter named like a state, an alias used next to a local variable named like its state, and states named _ and return.
• ErrorStateValues: the wrong-set error, a state name shared by two sets, and a state named like a generated set.
• TestStateHints#queryWrittenWithItsStateSetIsOfferedAsAGuard: a query written in the new form is still offered as a guard, so the state machine reads it.

The full suite passes locally. Found while testing: #509, an existing false error for a boolean query in an ordinary class, with either form.

🤖 Generated with Claude Code

[CatarinaGamboa]

Codex review, round 1 (codex exec review, this PR's commit only)

[P2] Resolve the state set by owner before rewriting (StateValues.java). When a subclass writes phase(this) == open for an inherited state set, the parser qualifies the call with the subclass name, so no set matches exactly. If another class also declares phase, this fallback selects whichever set appears first in the global state list.

Fixed. The rewrite no longer picks a set. It produces exactly the shorthand written in the same place: the set call's qualifier plus the state name, so a.Sub.door(this) == opened becomes a.Sub.opened(this). The later resolution therefore treats it like the shorthand, scoped to the variable's types and supertypes, in subclasses too. Matching against the sets only decides two things: whether the name is a state of some set with that name (rewrite), or a state of another set of the same class (error).

Regression: CorrectStateValueSubclass uses its superclass's door, while an unrelated class also declares a door with other states. Without the fix it fails with Sort mismatch ... CorrectStateValueDoor.door. The global list is in HashMap order, so the unrelated class is named to be listed first (commented in the fixture).

Clean-code review (clean-code-principles)

• core-dry / solid-srp: one helper, StateValues.toShorthand, with one job. Each parse site calls it through TypeChecker.readStateValues, which owns the "what is a variable here" rule (isVariableIn) and the error position. Alias bodies call it directly with their own parameters as scope.
• core-fail-fast: a state of another set is an error at the spec, not an unknown variable later. A missed parse site leaves an unknown variable, never a different meaning.
• name-meaningful: toShorthand, readStateValues, checkStatesAreNotInAnotherSet and qualifiedLike say what they do. namedSets became stateSets, since generated names are checked too now.
• func-small: registerGhostsAndStateSets grew one call; the new check is its own method.
• Tests: two fixtures and one hint assertion. Each case fails without the change, and the subclass case fails without the round 1 fix.

[CatarinaGamboa]

Codex review, round 2

[P1] Restrict state-set lookup to the referenced class (StateValues.java). When an unrelated class has a state set with the same simple name, matches() includes that set in this lookup. If the current class has door={closed} and lock={locked}, while another class has door={locked}, door(this) == locked is rewritten as locked(this) rather than rejected as a state from the wrong set.

Fixed. Only the sets that apply to the argument's type are considered, that is, sets declared on its class or a supertype. The type comes from where the spec is written:

• this is the class, or the refined class in an external spec;
• _ is the annotated element;
• a parameter, a variable of the context, or old(x) of one of those;
• in an alias body, the alias's declared parameter types, resolved the way AliasWrapper resolves them (that rule is now shared as AliasWrapper.parameterType).

When the type is unknown, the state is read only if every set of that name has it. If only some do, the name stays an unknown variable and gets the existing "not found" error, never a different meaning.

StateValues is now a small object holding the states, the variable test and the type test, which keeps the parameter lists short.

Regression: ErrorStateValuesOtherDoor, an unrelated door set that has a state locked. door(this) == locked is still the wrong-set error; before the fix it was silently read as locked(this).

[CatarinaGamboa]

Codex review, round 3

[P2] Resolve nested argument types before selecting state sets. When a refinement uses an expression such as door(getDoor()) == closed and another class declares a door set without closed, typeIn cannot determine the nested call's type, so both sets remain candidates and closed stays an unknown variable.

Declined: the shorthand does not support this either. Expression.substituteState translates a state only when its argument is a variable (fi.children.get(0) instanceof Var). So closed(getDoor()) is not given a meaning today, and door(getDoor()) == closed behaves the same way. It also fails safe: the name stays an unknown variable and gets the existing "not found" error, never a different meaning. Supporting non-variable state arguments would be a separate feature, for both forms.

No code change this round.

[CatarinaGamboa]

Codex review, round 4 (soundness only, the shorthand as the baseline)

[P2] A subclass's set can be rejected where its shorthand is valid. Base declares door = {open, closed} and Child extends Base declares door = {ajar, shut}. shut(this) is valid in Child, but door(this) == shut gives Variable 'shut' could not be found: both door sets apply to this, and only the child's has shut.

Fixed. The rule "every set of that name must have the state" is only needed when the argument's type is unknown. When it is known, the applicable sets are all in the argument's own class hierarchy, and the shorthand picks the state by name among them. So:

• type known: rewrite if any applicable set has the state;
• type unknown: rewrite only if every set of that name has it, as before.

The round 2 case still holds: an unrelated class's door does not apply to the type, so door(this) == locked is still the wrong-set error. StateValues now takes setsFor, which returns the sets that apply to an argument, or empty when its type is unknown.

Regression: CorrectStateValueBase / CorrectStateValueChild. It fails before this commit with Variable 'shut' could not be found.

[CatarinaGamboa]

Codex review, round 5

[P1] Preserve a field's own name before rewriting state values. @Refinement("phase(this) == open") int open; with a state open: the field is added to the context only after its annotation is parsed, so open would be read as the state.

Declined, no valid program reaches it. Both halves were checked on main, before this PR:

• That refinement is rejected before and after this PR with Variable 'this' could not be found: a field refinement cannot use this.
• Fields are not visible by their bare name in specs: @StateRefinement(from = "level == 2") with a field level gives Variable 'level' could not be found.

So a field named like a state never had a meaning that the rewrite could change. Treating every field as a variable would instead break the new form in a class that has a field named like one of its states, where the shorthand works. No code change.

[CatarinaGamboa]

Codex review, round 6

Codex was asked for programs that are valid on main and change meaning or verdict. It found two, both the two @StateSet checks this PR adds on purpose (#502, design round 6 and round 7):

• door = {open, closed} and lock = {open, locked} in one class is now an error, even when open is never used.
• @StateSet({"state2", "open"}) next to an unnamed second set, state2, is now an error, even when state2 is never used.

Kept, deliberately. In both, the shorthand (open(this), or the state state2 against the set function state2) cannot tell which one is meant, and today it silently picks one. Reporting it at the declaration is simpler and fails earlier than waiting for the first use. It is a breaking change only for specs with that ambiguity, so it is called out in the PR description for the maintainer to decide.

No code change. With rounds 5 and 6 reporting nothing else on the rewrite, the review loop for this PR is done.