[CatarinaGamboa]

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:

@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