liquid-java · CatarinaGamboa · May 7, 2026 · May 7, 2026
diff --git a/.gitignore b/.gitignore
@@ -15,7 +15,6 @@ CLAUDE.md
 
 # Local scripts and example scratch
 scripts/
-assets/examples/
 
 # Logs
 *.log
diff --git a/README.md b/README.md
@@ -1 +1,34 @@
-Webpage for liquidjava
+# liquid-java.github.io
+
+Source for the [LiquidJava](https://github.com/liquid-java) project website, served via GitHub Pages from `main`.
+
+## Local preview
+
+No build step, no package manager. Open `index.html` directly, or serve the directory:
+
+```sh
+python3 -m http.server 8000
+# then visit http://localhost:8000
+```
+
+## Structure
+
+- `index.html` — single-page site (markup, content, and inline JS for navbar + theme toggle).
+- `assets/css/style-starter.css` — vendored W3layouts template stylesheet plus LiquidJava overrides. Theme rules layered via `.light-theme` / `.dark-theme` on `<body>`.
+- `assets/js/jquery-3.3.1.min.js` — only JS dependency.
+- `assets/images/`, `assets/docs/`, `assets/extension/` — static assets (images, poster PDF, VSCode `.vsix`).
+
+## Theme toggle
+
+Dark/light mode is toggled by inline JS at the bottom of `index.html`. The selected theme is persisted in `localStorage` under the `theme` key and applied as a class on `<body>` before `DOMContentLoaded` to avoid a flash of unstyled content. When adding new sections, add explicit color rules for both themes in `style-starter.css`.
+
+## Deploying
+
+Push to `main`. GitHub Pages publishes the site automatically.
+
+## Related repositories
+
+- [`liquidjava`](https://github.com/liquid-java/liquidjava) — verifier, API, examples
+- [`liquidjava-docs`](https://github.com/liquid-java/liquidjava-docs) — documentation
+- [`liquidjava-tutorial`](https://github.com/liquid-java/liquidjava-tutorial) — tutorial
+- [`vscode-liquidjava`](https://github.com/liquid-java/vscode-liquidjava) — VSCode extension
diff --git a/assets/examples/data/abstract-undoable-edit/correct.java b/assets/examples/data/abstract-undoable-edit/correct.java
@@ -0,0 +1,6 @@
+// Path: aliveDone -> aliveNotDone -> aliveDone -> aliveNotDone -> aliveDone
+AbstractUndoableEdit edit = new AbstractUndoableEdit();
+edit.undo();
+edit.redo();
+edit.undo();
+edit.redo();
diff --git a/assets/examples/data/abstract-undoable-edit/incorrect.java b/assets/examples/data/abstract-undoable-edit/incorrect.java
@@ -0,0 +1,6 @@
+// Violation: redo() called twice in a row — second call is in state aliveDone.
+AbstractUndoableEdit edit = new AbstractUndoableEdit();
+edit.undo();
+edit.redo();
+edit.redo();   // INVALID: redo() requires aliveNotDone(edit),
+               //          but edit is in state aliveDone
diff --git a/assets/examples/data/abstract-undoable-edit/spec.java b/assets/examples/data/abstract-undoable-edit/spec.java
@@ -0,0 +1,16 @@
+@StateSet({"aliveDone", "aliveNotDone", "notAlive"})
+@ExternalRefinementsFor("javax.swing.undo.AbstractUndoableEdit")
+public interface AbstractUndoableEditRefinementsExpert {
+
+    @StateRefinement(to = "aliveDone(this)")
+    void AbstractUndoableEdit();
+
+    @StateRefinement(from = "aliveNotDone(this)", to = "aliveDone(this)")
+    void redo();
+
+    @StateRefinement(from = "aliveDone(this)", to = "aliveNotDone(this)")
+    void undo();
+
+    @StateRefinement(from = "!notAlive(this)", to = "notAlive(this)")
+    void die();
+}
diff --git a/assets/examples/data/abstract-undoable-edit/state.mmd b/assets/examples/data/abstract-undoable-edit/state.mmd
@@ -0,0 +1,7 @@
+stateDiagram-v2
+    [*] --> aliveDone : new AbstractUndoableEdit()
+    aliveDone --> aliveNotDone : undo()
+    aliveNotDone --> aliveDone : redo()
+    aliveDone --> notAlive : die()
+    aliveNotDone --> notAlive : die()
+    notAlive --> [*]
diff --git a/assets/examples/data/buffered-reader/correct.java b/assets/examples/data/buffered-reader/correct.java
@@ -0,0 +1,7 @@
+// Path: open -> open -> marked -> marked -> open -> open
+BufferedReader br = new BufferedReader(in);
+br.read();
+br.mark(42);
+br.read();
+br.reset();
+br.read();
diff --git a/assets/examples/data/buffered-reader/incorrect.java b/assets/examples/data/buffered-reader/incorrect.java
@@ -0,0 +1,7 @@
+// Violation: reset() called twice — second call is in state `open`.
+BufferedReader br = new BufferedReader(in);
+br.mark(42);
+br.read();
+br.reset();
+br.reset();   // INVALID: reset() requires marked(br),
+              //          but br is in state open
diff --git a/assets/examples/data/buffered-reader/spec.java b/assets/examples/data/buffered-reader/spec.java
@@ -0,0 +1,26 @@
+@RefinementAlias("NonNegative(int v) { v >= 0 }")
+@RefinementAlias("Positive(int v) { v > 0 }")
+@StateSet({"open", "marked", "closed"})
+@ExternalRefinementsFor("java.io.BufferedReader")
+public interface BufferedReaderRefinementsExpert {
+
+    @StateRefinement(to = "open(this)")
+    public void BufferedReader(Reader in);
+
+    @StateRefinement(to = "open(this)")
+    public void BufferedReader(Reader in, @Refinement("Positive(_)") int sz);
+
+    @StateRefinement(from = "open(this)")
+    @StateRefinement(from = "marked(this)")
+    public int read();
+
+    @StateRefinement(from = "open(this)", to = "marked(this)")
+    @StateRefinement(from = "marked(this)")
+    public void mark(@Refinement("NonNegative(_)") int readAheadLimit);
+
+    @StateRefinement(from = "marked(this)", to = "open(this)")
+    public void reset();
+
+    @StateRefinement(from = "!closed(this)", to = "closed(this)")
+    public void close();
+}
diff --git a/assets/examples/data/buffered-reader/state.mmd b/assets/examples/data/buffered-reader/state.mmd
@@ -0,0 +1,10 @@
+stateDiagram-v2
+    [*] --> open : new BufferedReader(in)
+    open --> open : read()
+    marked --> marked : read()
+    open --> marked : mark(n)
+    marked --> marked : mark(n)
+    marked --> open : reset()
+    open --> closed : close()
+    marked --> closed : close()
+    closed --> [*]
diff --git a/assets/examples/data/choice-callback/correct.java b/assets/examples/data/choice-callback/correct.java
@@ -0,0 +1,7 @@
+// Path: multiple -> multiple -> multiple
+// Constructor's last argument is `true`, so the SMT solver
+// concludes the result is in state `multiple`.
+ChoiceCallback cb = new ChoiceCallback(
+    "Pick options", new String[]{"a", "b"}, 0, true);
+cb.setSelectedIndexes(new int[]{0});
+cb.setSelectedIndexes(new int[]{0, 1});
diff --git a/assets/examples/data/choice-callback/incorrect.java b/assets/examples/data/choice-callback/incorrect.java
@@ -0,0 +1,6 @@
+// Violation: last constructor argument is `false` -> state `single`,
+// where setSelectedIndexes() is forbidden.
+ChoiceCallback cb = new ChoiceCallback(
+    "Pick one", new String[]{"a", "b"}, 0, false);
+cb.setSelectedIndexes(new int[]{0});   // INVALID: requires multiple(cb),
+                                       //          but cb is in state single
diff --git a/assets/examples/data/choice-callback/spec.java b/assets/examples/data/choice-callback/spec.java
@@ -0,0 +1,12 @@
+@StateSet({"single", "multiple"})
+@ExternalRefinementsFor("javax.security.auth.callback.ChoiceCallback")
+public interface ChoiceCallbackRefinementsExpert {
+
+    @StateRefinement(to = "multipleSelectionsAllowed ? multiple(this) : single(this)")
+    public void ChoiceCallback(String prompt, String[] choices,
+                               int defaultChoice,
+                               boolean multipleSelectionsAllowed);
+
+    @StateRefinement(from = "multiple(this)", to = "multiple(this)")
+    public void setSelectedIndexes(int[] selections);
+}
diff --git a/assets/examples/data/choice-callback/state.mmd b/assets/examples/data/choice-callback/state.mmd
@@ -0,0 +1,4 @@
+stateDiagram-v2
+    [*] --> single : new ChoiceCallback(..., false)
+    [*] --> multiple : new ChoiceCallback(..., true)
+    multiple --> multiple : setSelectedIndexes(s)
diff --git a/assets/examples/data/email/correct.java b/assets/examples/data/email/correct.java
@@ -0,0 +1,6 @@
+// Path: emptyEmail -> senderSet -> receiverSet -> receiverSet -> bodySet
+Email e = new Email();
+e.from("Alice");
+e.to("Bob");
+e.to("Carol");
+e.body("Hello!");
diff --git a/assets/examples/data/email/incorrect.java b/assets/examples/data/email/incorrect.java
@@ -0,0 +1,6 @@
+// Violation: to() called before from() — sender was never set.
+Email e = new Email();
+e.to("Bob");          // INVALID: requires senderSet or receiverSet,
+                      //          but e is still in emptyEmail
+e.from("Alice");
+e.body("Hello!");
diff --git a/assets/examples/data/email/spec.java b/assets/examples/data/email/spec.java
@@ -0,0 +1,20 @@
+@StateSet({"emptyEmail", "receiverSet", "senderSet", "bodySet"})
+public class Email {
+
+  @StateRefinement(to = "emptyEmail(this)")
+  public Email() {...}
+
+  @StateRefinement(from = "emptyEmail(this)", to = "senderSet(this)")
+  public void from(String s) {...}
+
+  @StateRefinement(from = "(senderSet(this)) || (receiverSet(this))",
+                   to   = "receiverSet(this)")
+  public void to(String s) {...}
+
+  @StateRefinement(from = "receiverSet(this)", to = "receiverSet(this)")
+  public void subject(String s) {...}
+
+  @StateRefinement(from = "receiverSet(this)", to = "bodySet(this)")
+  public void body(String s) {...}
+
+}
diff --git a/assets/examples/data/email/state.mmd b/assets/examples/data/email/state.mmd
@@ -0,0 +1,7 @@
+stateDiagram-v2
+    [*] --> emptyEmail : new Email()
+    emptyEmail --> senderSet : from(s)
+    senderSet --> receiverSet : to(s)
+    receiverSet --> receiverSet : to(s)
+    receiverSet --> receiverSet : subject(s)
+    receiverSet --> bodySet : body(s)
diff --git a/assets/examples/data/image-write-param/correct.java b/assets/examples/data/image-write-param/correct.java
@@ -0,0 +1,15 @@
+ImageWriteParam p = new ImageWriteParam(Locale.US);
+// state: startTiling && startCompression
+
+// --- Tiling axis: drive it independently ---
+p.setTilingMode(2);            // -> tilingExplicit
+p.setTiling(64, 64, 0, 0);     // -> tilingSet
+int w = p.getTileWidth();      // ok in tilingSet
+
+// --- Compression axis: still in startCompression, advance now ---
+p.setCompressionMode(2);       // -> compressionExplicit
+p.setCompressionType("JPEG");  // -> compressionSet
+String t = p.getCompressionType();
+
+// Order between axes doesn't matter — the two state machines
+// are orthogonal. Each method only constrains its own axis.
diff --git a/assets/examples/data/image-write-param/incorrect.java b/assets/examples/data/image-write-param/incorrect.java
@@ -0,0 +1,15 @@
+ImageWriteParam p = new ImageWriteParam(Locale.US);
+
+// Drive the tiling axis all the way to tilingSet...
+p.setTilingMode(2);            // -> tilingExplicit
+p.setTiling(64, 64, 0, 0);     // -> tilingSet
+int w = p.getTileWidth();      // ok
+
+// ...but the compression axis was never advanced.
+// It's still in startCompression — getCompressionType() needs
+// compressionExplicit or compressionSet.
+String type = p.getCompressionType();   // ✗ rejected
+
+// Violation: getCompressionType() requires compressionExplicit(this)
+// or compressionSet(this), but the compression axis is in state
+// startCompression.
diff --git a/assets/examples/data/image-write-param/spec.java b/assets/examples/data/image-write-param/spec.java
@@ -0,0 +1,39 @@
+// Two orthogonal @StateSet declarations describe two independent
+// state machines on the same object. The constructor places it in
+// the start state of BOTH axes; methods only constrain one axis.
+
+@StateSet({"startTiling", "tilingExplicit", "tilingSet"})
+@StateSet({"startCompression", "compressionExplicit", "compressionSet"})
+@ExternalRefinementsFor("javax.imageio.ImageWriteParam")
+public interface ImageWriteParamsRefinementsExpert {
+
+    @StateRefinement(to = "startTiling(this) && startCompression(this)")
+    void ImageWriteParam(Locale locale);
+
+    // ---- Tiling axis ----
+
+    @StateRefinement(to = "mode == 2 ? tilingExplicit(this) : startTiling(this)")
+    void setTilingMode(@Refinement("_ >= 0 && _ <= 3") int mode);
+
+    @StateRefinement(from = "tilingExplicit(this)", to = "tilingSet(this)")
+    @StateRefinement(from = "tilingSet(this)",       to = "tilingSet(this)")
+    void setTiling(@Refinement("_ > 0") int tileWidth,
+                   @Refinement("_ > 0") int tileHeight,
+                   int xOff, int yOff);
+
+    @StateRefinement(from = "tilingSet(this)") int getTileWidth();
+    @StateRefinement(from = "tilingSet(this)") int getTileHeight();
+
+    // ---- Compression axis ----
+
+    @StateRefinement(to = "mode == 2 ? compressionExplicit(this) : startCompression(this)")
+    void setCompressionMode(int mode);
+
+    @StateRefinement(from = "compressionExplicit(this)",
+                     to   = "compressionSet(this)")
+    void setCompressionType(String type);
+
+    @StateRefinement(from = "compressionExplicit(this)")
+    @StateRefinement(from = "compressionSet(this)")
+    String getCompressionType();
+}
diff --git a/assets/examples/data/image-write-param/state.mmd b/assets/examples/data/image-write-param/state.mmd
@@ -0,0 +1,20 @@
+stateDiagram-v2
+    direction LR
+
+    state "Tiling axis" as tiling {
+        [*] --> startTiling : new ImageWriteParam(locale)
+        startTiling --> tilingExplicit : setTilingMode(2)
+        tilingExplicit --> startTiling : setTilingMode(!=2)
+        tilingExplicit --> tilingSet : setTiling(w, h, ...)
+        tilingSet --> tilingSet : setTiling(...) / getTileWidth()
+        tilingSet --> startTiling : setTilingMode(!=2)
+    }
+
+    state "Compression axis" as compression {
+        [*] --> startCompression : new ImageWriteParam(locale)
+        startCompression --> compressionExplicit : setCompressionMode(2)
+        compressionExplicit --> startCompression : setCompressionMode(!=2)
+        compressionExplicit --> compressionSet : setCompressionType(...)
+        compressionSet --> compressionSet : getCompressionType()
+        compressionSet --> startCompression : setCompressionMode(!=2)
+    }
diff --git a/assets/examples/data/socket/correct.java b/assets/examples/data/socket/correct.java
@@ -0,0 +1,7 @@
+// Path: unconnected -> bound -> connected -> inputShutdown -> bothShutdown
+Socket s = new Socket();
+s.bind(addr);
+s.connect(endpoint);
+s.shutdownInput();
+s.shutdownOutput();
+s.close();
diff --git a/assets/examples/data/socket/incorrect.java b/assets/examples/data/socket/incorrect.java
@@ -0,0 +1,8 @@
+// Violation: setReuseAddress() is restricted to state `connected`,
+// but here it's called after shutdownInput() — i.e. in state `inputShutdown`.
+Socket s = new Socket();
+s.bind(addr);
+s.connect(endpoint);
+s.shutdownInput();
+s.setReuseAddress(true);   // INVALID: requires connected(s),
+                           //          but s is in state inputShutdown
diff --git a/assets/examples/data/socket/spec.java b/assets/examples/data/socket/spec.java
@@ -0,0 +1,34 @@
+@ExternalRefinementsFor("java.net.Socket")
+@RefinementAlias("Port(int x) { x >= 0 && x <= 65535 }")
+@StateSet({"unconnected", "bound", "connected",
+           "inputShutdown", "outputShutdown", "bothShutdown", "closed"})
+interface SocketRefinementsExpert {
+
+    @StateRefinement(to = "unconnected(this)")
+    void Socket();
+
+    @StateRefinement(to = "connected(this)")
+    void Socket(String host, @Refinement("Port(_)") int port);
+
+    @StateRefinement(from = "unconnected(this)", to = "bound(this)")
+    void bind(SocketAddress bindpoint);
+
+    @StateRefinement(from = "bound(this)", to = "connected(this)")
+    void connect(SocketAddress endpoint);
+
+    @StateRefinement(from = "connected(this)",     to = "inputShutdown(this)")
+    @StateRefinement(from = "outputShutdown(this)", to = "bothShutdown(this)")
+    public void shutdownInput();
+
+    @StateRefinement(from = "connected(this)",    to = "outputShutdown(this)")
+    @StateRefinement(from = "inputShutdown(this)", to = "bothShutdown(this)")
+    public void shutdownOutput();
+
+    @StateRefinement(from = "connected(this)")
+    public void setReuseAddress(boolean on);
+
+    @StateRefinement(from = "!closed(this)", to = "closed(this)")
+    public void close();
+
+    // ... ~30 more methods, mostly safe in any non-closed state
+}
diff --git a/assets/examples/data/socket/state.mmd b/assets/examples/data/socket/state.mmd
@@ -0,0 +1,16 @@
+stateDiagram-v2
+    [*] --> unconnected : new Socket()
+    [*] --> connected : new Socket(host, port)
+    unconnected --> bound : bind(addr)
+    bound --> connected : connect(endpoint)
+    connected --> inputShutdown : shutdownInput()
+    connected --> outputShutdown : shutdownOutput()
+    inputShutdown --> bothShutdown : shutdownOutput()
+    outputShutdown --> bothShutdown : shutdownInput()
+    unconnected --> closed : close()
+    bound --> closed : close()
+    connected --> closed : close()
+    inputShutdown --> closed : close()
+    outputShutdown --> closed : close()
+    bothShutdown --> closed : close()
+    closed --> [*]
diff --git a/assets/examples/data/throwable/correct.java b/assets/examples/data/throwable/correct.java
@@ -0,0 +1,3 @@
+// Path: noThrowable -> withThrowable
+Throwable t = new Throwable();
+t.initCause(cause);
diff --git a/assets/examples/data/throwable/incorrect.java b/assets/examples/data/throwable/incorrect.java
@@ -0,0 +1,4 @@
+// Violation: initCause() called on a Throwable that already has a cause.
+Throwable t = new Throwable("oops", cause);
+t.initCause(cause2);   // INVALID: initCause() requires noThrowable(t),
+                       //          but t is in state withThrowable