From 6a562cb5bfc4b9fee76a75e6a03f5a496e83fc56 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Mon, 9 Nov 2026 18:24:45 +0000 Subject: [PATCH] Document named state sets and states written as values of their sets Co-Authored-By: Claude Opus 5.5 --- README.md | 18 ++++++++++++------ 1 file changed, 12 insertions(+), 6 deletions(-) diff --git a/README.md b/README.md index 2a3cb879..f5e5d2a4 100644 --- a/README.md +++ b/README.md @@ -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(); } @@ -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: