Skip to content

Document named state sets and states written as values of their sets #512

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
CatarinaGamboa merged 1 commit into from
Nov 9, 2026
Merged

Document named state sets and states written as values of their sets #512

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
18 changes: 12 additions & 6 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -37,21 +37,21 @@ LiquidJava also supports object state modeling via typestates, which allows enfo

```java
@ExternalRefinementsFor("java.net.Socket")
@StateSet({"unconnected", "bound", "connected", "closed"})
@StateSet(name="connection", value={"unconnected", "bound", "connected", "closed"})
public interface SocketRefinements {
@StateRefinement(to="unconnected(this)")
@StateRefinement(to="connection(this) == unconnected")
public void Socket();

@StateRefinement(from="unconnected(this)", to="bound(this)")
@StateRefinement(from="connection(this) == unconnected", to="connection(this) == bound")
public void bind(SocketAddress add);

@StateRefinement(from="bound(this)", to="connected(this)")
@StateRefinement(from="connection(this) == bound", to="connection(this) == connected")
public void connect(SocketAddress add);

@StateRefinement(from="connected(this)")
@StateRefinement(from="connection(this) == connected")
public void sendUrgentData(int n);

@StateRefinement(from="!closed(this)", to="closed(this)")
@StateRefinement(from="connection(this) != closed", to="connection(this) == closed")
public void close();
}

Expand All @@ -61,6 +61,12 @@ socket.sendUrgentData(1); // State Refinement Error
socket.close();
```

A state set can be given a `name`, and a state is then written as a value of its set, `connection(this) == bound`. The shorter form `bound(this)` means the same and is also accepted. A class can have several state sets; a method's `to` keeps unchanged the sets it does not mention. Error messages show the states of named sets in the first form, so they say which set is in which state:

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

Lambda bodies are checked separately from the code that creates them. Creating a lambda does not apply its state
transitions to captured objects. While checking the body, LiquidJava keeps declared refinements but forgets the current
state of mutable captures, since that state may change before invocation. Callback execution summaries are not supported:
Expand Down
Loading