Skip to content

Expand aliases before translating states - #507

Merged
CatarinaGamboa merged 1 commit into
mainfrom
fix/503-alias-states
Nov 9, 2026
Merged

Expand aliases before translating states#507
CatarinaGamboa merged 1 commit into
mainfrom
fix/503-alias-states

Conversation

@CatarinaGamboa

@CatarinaGamboa CatarinaGamboa commented Nov 9, 2026

Copy link
Copy Markdown
Collaborator

Fixes #503

Cause. Before Z3, every refinement went through changeStatesToRefinements and then changeAliasToRefinement. A state that only appears once an alias is expanded, such as closed(x) in the body of Closed(x), was never translated to its state set. It stayed an uninterpreted Boolean unrelated to state1(x), so Closed(_) rejected a closed object.

Fix. One method, Predicate.toSolverPredicate, now does both steps in the right order: expand aliases, then translate states, then validate ghost invocations. Validation moves to the end so it sees the translated states. It replaces the six copies of the old pair in VCChecker and TypeChecker.

Before / after (ErrorStateInAlias):

Refinement Error: closed(door) is not a subtype of Closed(door)
  where Closed(x) = closed(x)

was reported at the first needsClosed(door), right after the constructor. Now that call verifies, and only the call after door.open() is reported.

This is also the step #502 relies on to translate phase(x) == closed in alias bodies.

Tests. ErrorStateInAlias: one call that must verify and one that must fail. On main the first call fails. Full suite passes locally.

🤖 Generated with Claude Code

@CatarinaGamboa @claude
Expand aliases before translating states, so a state in an alias body…
8b3c32b 
… is translated

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@CatarinaGamboa

CatarinaGamboa commented Nov 9, 2026

Copy link
Copy Markdown
Collaborator Author

Codex review, round 1 (codex exec review --base origin/main)

No actionable regressions were found. The new alias-state test produces its expected diagnostic, and the TestExamples suite passes.

Clean-code review (clean-code-principles)

Diff only, checked against the standing rules (smallest PR that tests well, match the surrounding code).

  • core-dry: the "states, then aliases" pair was copied six times across VCChecker and TypeChecker. Getting its order wrong was the bug, so the order now lives in one method.
  • name-meaningful: toSolverPredicate names what callers want, the predicate Z3 checks, rather than the two steps inside it.
  • solid-srp: the method only composes existing steps (changeAlias, changeStatesToRefinements, validateGhostInvocations); none of them changed.
  • func-few-arguments: four parameters, the union of the two old calls. A parameter object would add a type with one user, so no change.
  • Tests: one fixture that fails on main. Nothing redundant.

No changes needed.

This was referenced Nov 9, 2026
Open
Merged
Merged
Merged
@CatarinaGamboa
CatarinaGamboa merged commit 53f8b1d into main Nov 9, 2026
1 check passed
CatarinaGamboa added a commit that referenced this pull request Nov 9, 2026
@CatarinaGamboa @claude
Accept a state written as a value of its set: phase(this) == open (#510)
7236063 
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:

```java
@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 #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](https://claude.com/claude-code)

---------

Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
CatarinaGamboa added a commit that referenced this pull request Nov 9, 2026
@CatarinaGamboa @claude
Show the states of named sets as values of their sets in state errors (…
9d8ccad 
…#511)

Part of #502 (PR 2, messages). **Depends on #510**, which depends on
#507 and #508. Only the last commit belongs here.

## What

State errors show the states of **named** sets as values of their sets,
whichever form the spec used. `ErrorStateHintMultipleSets` (sets
`doorState` and `lockState`):

```
- found closed(d@26) && locked(d) && doorState(d) == doorState(d@26) but expected closed(d) && unlocked(d)
+ found doorState(d@26) == closed && lockState(d) == locked && doorState(d) == doorState(d@26) but expected doorState(d) == closed && lockState(d) == unlocked
```

It is now plain which set fails (only `lockState`), and the frame
equality chains on its own: `doorState(d) == doorState(d@26)` and
`doorState(d@26) == closed`.

`!open(x)` is shown as `door(x) != open`. A state keeps the shorthand
when its set has a generated name (`state2(x) == closed` reads worse
than `closed(x)`), or when sets with different names have a state of
that name. That way the set printed is never a guess.

## How

`StateValues.toSetForm` rewrites expressions for display only.
`StateRefinementError` receives it as `display`:
- **The facts to show are still chosen on the expressions as given.**
`linkedToExpected` and #495's relevance step run first. A shared state
name such as `closed`, which is a variable in the rewritten form, would
otherwise link facts about unrelated objects.
- The message, `getExpected()` and every derivation step
(`VCSimplificationResult.map`) hold the rewritten form, so the **IDE
shows it without a server change**: the server formats those expressions
as they are.

Nothing the verifier decides changes: the VC, the verdict, the hints and
the category are the same. Refinement errors (`RefinementError`) keep
the shorthand for now. They also build alias expansions and
counterexamples from the same expressions, so that would be its own
change.

`Formats.STATE_SET` names the generated `stateN`, which the display
needs to recognise.

## Tests
- `TestStateHints#foundKeepsANamedStateSetByItsName`: the message above.
It fails without the change.

The full suite passes locally.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

---------

Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
CatarinaGamboa added a commit that referenced this pull request Nov 9, 2026
@CatarinaGamboa @claude
Document named state sets and states written as values of their sets (#…
70472eb 
…512)

Part of #502 (PR 3, docs). **Depends on #511** (and so on #510, #508 and
#507). Only the last commit belongs here.

The README's typestate example now names its set and writes states as
values of it:

```java
@stateset(name="connection", value={"unconnected", "bound", "connected", "closed"})
...
@StateRefinement(from="connection(this) == unconnected", to="connection(this) == bound")
public void bind(SocketAddress add);
...
@StateRefinement(from="connection(this) != closed", to="connection(this) == closed")
public void close();
```

A short paragraph says that the shorthand `bound(this)` is still
accepted, that a `to` keeps the sets it does not mention, and what the
error looks like. That error was checked by running the README example
on #511:

```
State Refinement Error: found connection(socket) == bound but expected connection(socket) == connected
```

The study exercises live in the study repository and are not changed
here.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

False error: a state inside a @RefinementAlias body is not translated (Closed(_) rejects a closed object)

1 participant

@CatarinaGamboa