From 7ab09812994fb7429fe07a95db3990f96ddf632b Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 5 Oct 2026 16:22:22 +0100 Subject: [PATCH] Verify website examples in the browser Co-authored-by: OpenAI Codex --- .github/workflows/pages.yml | 65 +++++ .gitignore | 7 + README.md | 18 +- assets/css/style-starter.css | 22 +- .../data/abstract-undoable-edit/correct.java | 18 +- .../abstract-undoable-edit/incorrect.java | 18 +- .../data/abstract-undoable-edit/spec.java | 3 + .../data/buffered-reader/correct.java | 21 +- .../data/buffered-reader/incorrect.java | 21 +- .../examples/data/buffered-reader/spec.java | 4 + .../data/choice-callback/correct.java | 20 +- .../data/choice-callback/incorrect.java | 18 +- .../examples/data/choice-callback/spec.java | 3 + assets/examples/data/email/correct.java | 17 +- assets/examples/data/email/incorrect.java | 17 +- assets/examples/data/email/spec.java | 12 +- .../data/image-write-param/correct.java | 31 +- .../data/image-write-param/incorrect.java | 31 +- .../examples/data/image-write-param/spec.java | 4 + assets/examples/data/socket/correct.java | 21 +- assets/examples/data/socket/incorrect.java | 23 +- assets/examples/data/socket/spec.java | 4 + assets/examples/data/throwable/correct.java | 11 +- assets/examples/data/throwable/incorrect.java | 13 +- assets/examples/data/throwable/spec.java | 2 + assets/examples/data/uuid/correct.java | 18 +- assets/examples/data/uuid/incorrect.java | 18 +- assets/examples/data/uuid/spec.java | 3 + assets/examples/data/zip-file/correct.java | 21 +- assets/examples/data/zip-file/incorrect.java | 23 +- assets/examples/data/zip-file/spec.java | 8 + assets/examples/examples.json | 27 +- assets/js/gallery.js | 270 ++++++++++++++++++ index.html | 255 +---------------- 34 files changed, 655 insertions(+), 412 deletions(-) create mode 100644 .github/workflows/pages.yml create mode 100644 assets/js/gallery.js diff --git a/.github/workflows/pages.yml b/.github/workflows/pages.yml new file mode 100644 index 0000000..1e29c6b --- /dev/null +++ b/.github/workflows/pages.yml @@ -0,0 +1,65 @@ +name: Build and deploy website +on: + push: + branches: [main] + pull_request: + workflow_dispatch: +permissions: + contents: read +concurrency: + group: pages-${{ github.event.pull_request.number || 'deploy' }} + cancel-in-progress: true +jobs: + build: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - uses: actions/setup-node@v4 + with: + node-version: "22" + - name: Check out shared browser verifier + uses: actions/checkout@v4 + with: + repository: liquid-java/liquidjava-docs + ref: 7b61cdde7010b06629c4cdaf298e5b54daba4f63 + path: .browser-source + + - name: Set up Java + uses: actions/setup-java@v4 + with: + distribution: temurin + java-version: "17" + + - name: Build shared browser verifier + working-directory: .browser-source + run: | + npm ci --ignore-scripts --no-audit --no-fund + npm run build:playground + npm run test:playground + node scripts/playground/export.mjs .. + + - name: Check gallery script + run: node --check assets/js/gallery.js + - name: Stage website + run: | + mkdir _site + cp index.html robots.txt sitemap.xml llms.txt _headers .nojekyll isolation.js _site/ + cp -R assets .well-known verifier _site/ + - uses: actions/upload-pages-artifact@v3 + if: github.event_name != 'pull_request' + with: + path: _site + deploy: + if: github.event_name != 'pull_request' + needs: build + runs-on: ubuntu-latest + permissions: + pages: write + id-token: write + environment: + name: github-pages + url: ${{ steps.deployment.outputs.page_url }} + steps: + - uses: actions/configure-pages@v5 + - uses: actions/deploy-pages@v4 + id: deployment diff --git a/.gitignore b/.gitignore index a6a3ddf..35c957a 100644 --- a/.gitignore +++ b/.gitignore @@ -18,3 +18,10 @@ scripts/ # Logs *.log + +# generated browser runtime +verifier/ +isolation.js +.browser-source/ + +_site/ diff --git a/README.md b/README.md index 748da6a..4f2b560 100644 --- a/README.md +++ b/README.md @@ -4,18 +4,24 @@ Source for the [LiquidJava](https://github.com/liquid-java) project website, ser ## Local preview -No build step, no package manager. Open `index.html` directly, or serve the directory: +Build the shared verifier in the adjacent docs checkout with JDK 17, then export it here: ```sh -python3 -m http.server 8000 -# then visit http://localhost:8000 +cd ../liquidjava-docs +npm ci +npm run build:playground +node scripts/playground/export.mjs ../liquid-java.github.io +node node_modules/http-server/bin/http-server ../liquid-java.github.io -p 8001 -c-1 ``` +Open `http://localhost:8001`. Use HTTPS or localhost and a server with HTTP range support for the JARs. The isolation service worker reloads once; the verifier itself loads on the first Run. Each usage is checked together with its displayed specification, locally in a worker. Results contain only diagnostic titles and messages. Stop, changing examples, and changing tabs cancel pending verification. + ## 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 ``. -- `assets/js/jquery-3.3.1.min.js` — only JS dependency. +- `assets/js/gallery.js` — gallery selection and browser verification. +- `assets/js/jquery-3.3.1.min.js` — vendored jQuery. - `assets/images/`, `assets/docs/`, `assets/extension/` — static assets (images, poster PDF, VSCode `.vsix`). ## Theme toggle @@ -24,7 +30,7 @@ Dark/light mode is toggled by inline JS at the bottom of `index.html`. The selec ## Deploying -Push to `main`. GitHub Pages publishes the site automatically. +Select **GitHub Actions** as the Pages build source. The Pages workflow builds the runtime from a pinned commit of `liquid-java/liquidjava-docs`, validates it, and publishes the static site on pushes to `main`. Update the checkout `ref` after testing a shared-runtime upgrade. Generated `verifier/` and `isolation.js` files are ignored by Git. ## Related repositories @@ -32,3 +38,5 @@ Push to `main`. GitHub Pages publishes the site automatically. - [`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 + +The introduction video opens on YouTube because the cross-origin isolation required by the verifier prevents embedding its player. Neighboring GitHub Pages projects are excluded from the root isolation worker’s navigation responses. diff --git a/assets/css/style-starter.css b/assets/css/style-starter.css index bb71f75..781b2eb 100644 --- a/assets/css/style-starter.css +++ b/assets/css/style-starter.css @@ -12416,24 +12416,6 @@ body:after { margin-left: -12%; } -.iframe_container{ - position: relative; - overflow: hidden; - width: 100%; - padding-top: 56.25%; /* 16:9 Aspect Ratio (divide 9 by 16 = 0.5625) */ -} - -/* Then style the iframe to fit in the container div with full height and width */ -.responsive-iframe { - position: absolute; - top: 0; - left: 0; - bottom: 0; - right: 0; - width: 100%; - height: 100%; -} - .small_p { margin: 1%!important; } @@ -13903,3 +13885,7 @@ body.dark-theme .lj-resource-card--muted .lj-resource-icon { background: transpa .lj-steps { grid-template-columns: 1fr; gap: 1.6rem; } .lj-install-title { font-size: 1.55rem; } } + +.lj-verifier-body p { margin: 0 0 0.75rem; } +.lj-verifier-body p:last-child { margin-bottom: 0; } +.lj-run:disabled { opacity: 0.6; cursor: wait; } diff --git a/assets/examples/data/abstract-undoable-edit/correct.java b/assets/examples/data/abstract-undoable-edit/correct.java index 06f20ef..7277fe7 100644 --- a/assets/examples/data/abstract-undoable-edit/correct.java +++ b/assets/examples/data/abstract-undoable-edit/correct.java @@ -1,6 +1,12 @@ -// Path: aliveDone -> aliveNotDone -> aliveDone -> aliveNotDone -> aliveDone -AbstractUndoableEdit edit = new AbstractUndoableEdit(); -edit.undo(); -edit.redo(); -edit.undo(); -edit.redo(); +import javax.swing.undo.AbstractUndoableEdit; + +class Example { + static void example() throws Exception { + // 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 index 2c936f2..7b56903 100644 --- a/assets/examples/data/abstract-undoable-edit/incorrect.java +++ b/assets/examples/data/abstract-undoable-edit/incorrect.java @@ -1,6 +1,12 @@ -// 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 +import javax.swing.undo.AbstractUndoableEdit; + +class Example { + static void example() throws Exception { + // 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 index 7536d57..ebc0f63 100644 --- a/assets/examples/data/abstract-undoable-edit/spec.java +++ b/assets/examples/data/abstract-undoable-edit/spec.java @@ -1,3 +1,6 @@ +import liquidjava.specification.*; +import javax.swing.undo.AbstractUndoableEdit; + @StateSet({"aliveDone", "aliveNotDone", "notAlive"}) @ExternalRefinementsFor("javax.swing.undo.AbstractUndoableEdit") public interface AbstractUndoableEditRefinementsExpert { diff --git a/assets/examples/data/buffered-reader/correct.java b/assets/examples/data/buffered-reader/correct.java index e1d5224..dc5e8f1 100644 --- a/assets/examples/data/buffered-reader/correct.java +++ b/assets/examples/data/buffered-reader/correct.java @@ -1,7 +1,14 @@ -// Path: open -> open -> marked -> marked -> open -> open -BufferedReader br = new BufferedReader(in); -br.read(); -br.mark(42); -br.read(); -br.reset(); -br.read(); +import java.io.BufferedReader; +import java.io.Reader; + +class Example { + static void example(Reader in) throws Exception { + // 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 index 83f81e9..744602b 100644 --- a/assets/examples/data/buffered-reader/incorrect.java +++ b/assets/examples/data/buffered-reader/incorrect.java @@ -1,7 +1,14 @@ -// 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 +import java.io.BufferedReader; +import java.io.Reader; + +class Example { + static void example(Reader in) throws Exception { + // 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 index bb7bc0b..c0cfa10 100644 --- a/assets/examples/data/buffered-reader/spec.java +++ b/assets/examples/data/buffered-reader/spec.java @@ -1,3 +1,7 @@ +import liquidjava.specification.*; +import java.io.BufferedReader; +import java.io.Reader; + @RefinementAlias("NonNegative(int v) { v >= 0 }") @RefinementAlias("Positive(int v) { v > 0 }") @StateSet({"open", "marked", "closed"}) diff --git a/assets/examples/data/choice-callback/correct.java b/assets/examples/data/choice-callback/correct.java index 616f4fe..92bd164 100644 --- a/assets/examples/data/choice-callback/correct.java +++ b/assets/examples/data/choice-callback/correct.java @@ -1,7 +1,13 @@ -// 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}); +import javax.security.auth.callback.ChoiceCallback; + +class Example { + static void example() throws Exception { + // 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 index dd4fdb2..4bc3e5d 100644 --- a/assets/examples/data/choice-callback/incorrect.java +++ b/assets/examples/data/choice-callback/incorrect.java @@ -1,6 +1,12 @@ -// 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 +import javax.security.auth.callback.ChoiceCallback; + +class Example { + static void example() throws Exception { + // 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 index 30e2955..45d8a7f 100644 --- a/assets/examples/data/choice-callback/spec.java +++ b/assets/examples/data/choice-callback/spec.java @@ -1,3 +1,6 @@ +import liquidjava.specification.*; +import javax.security.auth.callback.ChoiceCallback; + @StateSet({"single", "multiple"}) @ExternalRefinementsFor("javax.security.auth.callback.ChoiceCallback") public interface ChoiceCallbackRefinementsExpert { diff --git a/assets/examples/data/email/correct.java b/assets/examples/data/email/correct.java index 61880df..0c1b53a 100644 --- a/assets/examples/data/email/correct.java +++ b/assets/examples/data/email/correct.java @@ -1,6 +1,11 @@ -// Path: emptyEmail -> senderSet -> receiverSet -> receiverSet -> bodySet -Email e = new Email(); -e.from("Alice"); -e.to("Bob"); -e.to("Carol"); -e.body("Hello!"); + +class Example { + static void example() throws Exception { + // 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 index cabbaae..7b111e3 100644 --- a/assets/examples/data/email/incorrect.java +++ b/assets/examples/data/email/incorrect.java @@ -1,6 +1,11 @@ -// 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!"); + +class Example { + static void example() throws Exception { + // 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 index 6682c87..fadb391 100644 --- a/assets/examples/data/email/spec.java +++ b/assets/examples/data/email/spec.java @@ -1,20 +1,22 @@ +import liquidjava.specification.*; + @StateSet({"emptyEmail", "receiverSet", "senderSet", "bodySet"}) public class Email { @StateRefinement(to = "emptyEmail(this)") - public Email() {...} + public Email() {} @StateRefinement(from = "emptyEmail(this)", to = "senderSet(this)") - public void from(String s) {...} + public void from(String s) {} @StateRefinement(from = "(senderSet(this)) || (receiverSet(this))", to = "receiverSet(this)") - public void to(String s) {...} + public void to(String s) {} @StateRefinement(from = "receiverSet(this)", to = "receiverSet(this)") - public void subject(String s) {...} + public void subject(String s) {} @StateRefinement(from = "receiverSet(this)", to = "bodySet(this)") - public void body(String s) {...} + public void body(String s) {} } diff --git a/assets/examples/data/image-write-param/correct.java b/assets/examples/data/image-write-param/correct.java index f32a70a..302bf19 100644 --- a/assets/examples/data/image-write-param/correct.java +++ b/assets/examples/data/image-write-param/correct.java @@ -1,15 +1,22 @@ -ImageWriteParam p = new ImageWriteParam(Locale.US); -// state: startTiling && startCompression +import javax.imageio.ImageWriteParam; +import java.util.Locale; -// --- Tiling axis: drive it independently --- -p.setTilingMode(2); // -> tilingExplicit -p.setTiling(64, 64, 0, 0); // -> tilingSet -int w = p.getTileWidth(); // ok in tilingSet +class Example { + static void example() throws Exception { + ImageWriteParam p = new ImageWriteParam(Locale.US); + // state: startTiling && startCompression -// --- Compression axis: still in startCompression, advance now --- -p.setCompressionMode(2); // -> compressionExplicit -p.setCompressionType("JPEG"); // -> compressionSet -String t = p.getCompressionType(); + // --- Tiling axis: drive it independently --- + p.setTilingMode(2); // -> tilingExplicit + p.setTiling(64, 64, 0, 0); // -> tilingSet + int w = p.getTileWidth(); // ok in tilingSet -// Order between axes doesn't matter — the two state machines -// are orthogonal. Each method only constrains its own axis. + // --- 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 index d87a929..58fc128 100644 --- a/assets/examples/data/image-write-param/incorrect.java +++ b/assets/examples/data/image-write-param/incorrect.java @@ -1,15 +1,22 @@ -ImageWriteParam p = new ImageWriteParam(Locale.US); +import javax.imageio.ImageWriteParam; +import java.util.Locale; -// 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 +class Example { + static void example() throws Exception { + ImageWriteParam p = new ImageWriteParam(Locale.US); -// ...but the compression axis was never advanced. -// It's still in startCompression — getCompressionType() needs -// compressionExplicit or compressionSet. -String type = p.getCompressionType(); // ✗ rejected + // 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 -// Violation: getCompressionType() requires compressionExplicit(this) -// or compressionSet(this), but the compression axis is in state -// startCompression. + // ...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 index c894363..b960569 100644 --- a/assets/examples/data/image-write-param/spec.java +++ b/assets/examples/data/image-write-param/spec.java @@ -1,3 +1,7 @@ +import liquidjava.specification.*; +import javax.imageio.ImageWriteParam; +import java.util.Locale; + // 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. diff --git a/assets/examples/data/socket/correct.java b/assets/examples/data/socket/correct.java index 6026b93..a035890 100644 --- a/assets/examples/data/socket/correct.java +++ b/assets/examples/data/socket/correct.java @@ -1,7 +1,14 @@ -// Path: unconnected -> bound -> connected -> inputShutdown -> bothShutdown -Socket s = new Socket(); -s.bind(addr); -s.connect(endpoint); -s.shutdownInput(); -s.shutdownOutput(); -s.close(); +import java.net.Socket; +import java.net.SocketAddress; + +class Example { + static void example(SocketAddress addr, SocketAddress endpoint) throws Exception { + // 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 index 26ba038..5c959e0 100644 --- a/assets/examples/data/socket/incorrect.java +++ b/assets/examples/data/socket/incorrect.java @@ -1,8 +1,15 @@ -// 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 +import java.net.Socket; +import java.net.SocketAddress; + +class Example { + static void example(SocketAddress addr, SocketAddress endpoint) throws Exception { + // 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 index fbceef5..6a035b0 100644 --- a/assets/examples/data/socket/spec.java +++ b/assets/examples/data/socket/spec.java @@ -1,3 +1,7 @@ +import liquidjava.specification.*; +import java.net.Socket; +import java.net.SocketAddress; + @ExternalRefinementsFor("java.net.Socket") @RefinementAlias("Port(int x) { x >= 0 && x <= 65535 }") @StateSet({"unconnected", "bound", "connected", diff --git a/assets/examples/data/throwable/correct.java b/assets/examples/data/throwable/correct.java index f7c1c74..b9a40b7 100644 --- a/assets/examples/data/throwable/correct.java +++ b/assets/examples/data/throwable/correct.java @@ -1,3 +1,8 @@ -// Path: noThrowable -> withThrowable -Throwable t = new Throwable(); -t.initCause(cause); + +class Example { + static void example(Throwable cause, Throwable cause2) throws Exception { + // 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 index 58cc2a7..1eb2ae5 100644 --- a/assets/examples/data/throwable/incorrect.java +++ b/assets/examples/data/throwable/incorrect.java @@ -1,4 +1,9 @@ -// 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 + +class Example { + static void example(Throwable cause, Throwable cause2) throws Exception { + // 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 + } +} diff --git a/assets/examples/data/throwable/spec.java b/assets/examples/data/throwable/spec.java index 9e85a25..100ba82 100644 --- a/assets/examples/data/throwable/spec.java +++ b/assets/examples/data/throwable/spec.java @@ -1,3 +1,5 @@ +import liquidjava.specification.*; + @StateSet({"withThrowable", "noThrowable"}) @ExternalRefinementsFor("java.lang.Throwable") public interface ThrowableRefinementsExpert { diff --git a/assets/examples/data/uuid/correct.java b/assets/examples/data/uuid/correct.java index e239f29..c2c9ee0 100644 --- a/assets/examples/data/uuid/correct.java +++ b/assets/examples/data/uuid/correct.java @@ -1,6 +1,12 @@ -// Path: timeBased -> timeBased -> timeBased -// 4096 / 4096 == 1, and 1 % 16 == 1, so the predicate holds: -// the SMT solver picks the `timeBased` branch of the ternary. -UUID u = new UUID(4096L, 42L); -u.clockSequence(); -u.clockSequence(); +import java.util.UUID; + +class Example { + static void example() throws Exception { + // Path: timeBased -> timeBased -> timeBased + // 4096 / 4096 == 1, and 1 % 16 == 1, so the predicate holds: + // the SMT solver picks the `timeBased` branch of the ternary. + UUID u = new UUID(4096L, 42L); + u.clockSequence(); + u.clockSequence(); + } +} diff --git a/assets/examples/data/uuid/incorrect.java b/assets/examples/data/uuid/incorrect.java index f17917e..ea586a1 100644 --- a/assets/examples/data/uuid/incorrect.java +++ b/assets/examples/data/uuid/incorrect.java @@ -1,6 +1,12 @@ -// Violation: 42 / 4096 == 0, so (0 % 16 == 1) is false — -// the SMT solver picks the `dceSecurityNameRandom` branch, -// where clockSequence() is forbidden. -UUID u = new UUID(42L, 42L); -u.clockSequence(); // INVALID: requires maybeTime(u) or timeBased(u), - // but u is in state dceSecurityNameRandom +import java.util.UUID; + +class Example { + static void example() throws Exception { + // Violation: 42 / 4096 == 0, so (0 % 16 == 1) is false — + // the SMT solver picks the `dceSecurityNameRandom` branch, + // where clockSequence() is forbidden. + UUID u = new UUID(42L, 42L); + u.clockSequence(); // INVALID: requires maybeTime(u) or timeBased(u), + // but u is in state dceSecurityNameRandom + } +} diff --git a/assets/examples/data/uuid/spec.java b/assets/examples/data/uuid/spec.java index 9352cb6..69ec552 100644 --- a/assets/examples/data/uuid/spec.java +++ b/assets/examples/data/uuid/spec.java @@ -1,3 +1,6 @@ +import liquidjava.specification.*; +import java.util.UUID; + @ExternalRefinementsFor("java.util.UUID") @StateSet({"dceSecurityNameRandom", "maybeTime", "timeBased"}) @RefinementAlias("Version(int v) { v >= 0 && v <= 4 }") diff --git a/assets/examples/data/zip-file/correct.java b/assets/examples/data/zip-file/correct.java index ae042c9..4469ed0 100644 --- a/assets/examples/data/zip-file/correct.java +++ b/assets/examples/data/zip-file/correct.java @@ -1,5 +1,16 @@ -// Path: opened -> opened -> opened -> closed -ZipFile zip = new ZipFile(new File("test.zip")); -zip.entries(); -zip.entries(); -zip.close(); +import java.io.File; +import java.io.InputStream; +import java.util.Enumeration; +import java.util.stream.Stream; +import java.util.zip.ZipFile; +import java.util.zip.ZipEntry; + +class Example { + static void example() throws Exception { + // Path: opened -> opened -> opened -> closed + ZipFile zip = new ZipFile(new File("test.zip")); + zip.entries(); + zip.entries(); + zip.close(); + } +} diff --git a/assets/examples/data/zip-file/incorrect.java b/assets/examples/data/zip-file/incorrect.java index 28b65ad..64f01fd 100644 --- a/assets/examples/data/zip-file/incorrect.java +++ b/assets/examples/data/zip-file/incorrect.java @@ -1,6 +1,17 @@ -// Violation: stream() called after close() — use-after-close. -ZipFile zip = new ZipFile(new File("test.zip")); -zip.entries(); -zip.close(); -zip.stream(); // INVALID: stream() requires opened(zip), - // but zip is in state closed +import java.io.File; +import java.io.InputStream; +import java.util.Enumeration; +import java.util.stream.Stream; +import java.util.zip.ZipFile; +import java.util.zip.ZipEntry; + +class Example { + static void example() throws Exception { + // Violation: stream() called after close() — use-after-close. + ZipFile zip = new ZipFile(new File("test.zip")); + zip.entries(); + zip.close(); + zip.stream(); // INVALID: stream() requires opened(zip), + // but zip is in state closed + } +} diff --git a/assets/examples/data/zip-file/spec.java b/assets/examples/data/zip-file/spec.java index e8e96f4..fbdf430 100644 --- a/assets/examples/data/zip-file/spec.java +++ b/assets/examples/data/zip-file/spec.java @@ -1,3 +1,11 @@ +import liquidjava.specification.*; +import java.io.File; +import java.io.InputStream; +import java.util.Enumeration; +import java.util.stream.Stream; +import java.util.zip.ZipFile; +import java.util.zip.ZipEntry; + @ExternalRefinementsFor("java.util.zip.ZipFile") @StateSet({"opened", "closed"}) @RefinementAlias("Mode(int x){ x == 1 || x == 4 || x == 5 }") diff --git a/assets/examples/examples.json b/assets/examples/examples.json index 7d218c8..39688bd 100644 --- a/assets/examples/examples.json +++ b/assets/examples/examples.json @@ -5,8 +5,7 @@ "className": "Email (built-in tutorial)", "complexity": "simple", "factors": ["typestate"], - "blurb": "A four-step protocol for composing an email: sender, then recipient, then optional subject, then body. Hand-authored to introduce @StateSet and @StateRefinement.", - "violation": "Calling to(\"Bob\") in state emptyEmail; required: senderSet(this) or receiverSet(this)." + "blurb": "A four-step protocol for composing an email: sender, then recipient, then optional subject, then body. Hand-authored to introduce @StateSet and @StateRefinement." }, { "id": "abstract-undoable-edit", @@ -14,8 +13,7 @@ "className": "javax.swing.undo.AbstractUndoableEdit", "complexity": "simple", "factors": ["typestate"], - "blurb": "An edit alternates between aliveDone and aliveNotDone before being killed. Calling redo() while already done is a protocol error.", - "violation": "redo() requires aliveNotDone(this), but this is in state aliveDone." + "blurb": "An edit alternates between aliveDone and aliveNotDone before being killed. Calling redo() while already done is a protocol error." }, { "id": "zip-file", @@ -23,8 +21,7 @@ "className": "java.util.zip.ZipFile", "complexity": "simple", "factors": ["typestate"], - "blurb": "Open a zip, read entries, then close it. Touching a closed ZipFile is a use-after-close bug.", - "violation": "stream() requires opened(this), but this is in state closed." + "blurb": "Open a zip, read entries, then close it. Touching a closed ZipFile is a use-after-close bug." }, { "id": "throwable", @@ -32,8 +29,7 @@ "className": "java.lang.Throwable", "complexity": "simple", "factors": ["typestate"], - "blurb": "initCause() is only legal once — on a Throwable created without a cause. Calling it on one that already has a cause throws at runtime; LiquidJava catches it statically.", - "violation": "initCause() requires noThrowable(this), but this is in state withThrowable." + "blurb": "initCause() is only legal once — on a Throwable created without a cause. Calling it on one that already has a cause throws at runtime; LiquidJava catches it statically." }, { "id": "choice-callback", @@ -41,8 +37,7 @@ "className": "javax.security.auth.callback.ChoiceCallback", "complexity": "moderate", "factors": ["typestate", "conditional"], - "blurb": "The constructor lands in single or multiple based on a boolean argument. setSelectedIndexes() is only valid in multiple. The transition is conditional on a parameter value — a ternary in the spec.", - "violation": "setSelectedIndexes() requires multiple(this), but this is in state single." + "blurb": "The constructor lands in single or multiple based on a boolean argument. setSelectedIndexes() is only valid in multiple. The transition is conditional on a parameter value — a ternary in the spec." }, { "id": "image-write-param", @@ -50,8 +45,7 @@ "className": "javax.imageio.ImageWriteParam", "complexity": "complex", "factors": ["typestate", "orthogonal", "conditional"], - "blurb": "Two independent state machines on the same object: a tiling axis and a compression axis, each with its own (start → explicit → set) progression. Calls on one axis don't perturb the other.", - "violation": "getCompressionType() requires compressionExplicit(this) or compressionSet(this), but the compression axis is in state startCompression." + "blurb": "Two independent state machines on the same object: a tiling axis and a compression axis, each with its own (start → explicit → set) progression. Calls on one axis don't perturb the other." }, { "id": "buffered-reader", @@ -59,8 +53,7 @@ "className": "java.io.BufferedReader", "complexity": "complex", "factors": ["typestate"], - "blurb": "open ⇄ marked, both heading to closed. reset() only works after a mark(); double-resetting is a classic mistake.", - "violation": "reset() requires marked(this), but this is in state open." + "blurb": "open ⇄ marked, both heading to closed. reset() only works after a mark(); double-resetting is a classic mistake." }, { "id": "socket", @@ -68,8 +61,7 @@ "className": "java.net.Socket", "complexity": "complex", "factors": ["typestate"], - "blurb": "Six states: unconnected, bound, connected, inputShutdown, outputShutdown, bothShutdown, closed. Many setters are restricted to the connected state.", - "violation": "setReuseAddress() requires connected(this), but this is in state inputShutdown." + "blurb": "Six states: unconnected, bound, connected, inputShutdown, outputShutdown, bothShutdown, closed. Many setters are restricted to the connected state." }, { "id": "uuid", @@ -77,7 +69,6 @@ "className": "java.util.UUID", "complexity": "complex", "factors": ["refinement", "typestate"], - "blurb": "The classifier is bit-math on the constructor argument: (mostSigBits/4096) % 16 == 1 → timeBased, else dceSecurityNameRandom. clockSequence() is rejected on the random branch — an SMT predicate decides which state you're in.", - "violation": "clockSequence() requires maybeTime(this) or timeBased(this), but this is in state dceSecurityNameRandom." + "blurb": "The classifier is bit-math on the constructor argument: (mostSigBits/4096) % 16 == 1 → timeBased, else dceSecurityNameRandom. clockSequence() is rejected on the random branch — an SMT predicate decides which state you're in." } ] diff --git a/assets/js/gallery.js b/assets/js/gallery.js new file mode 100644 index 0000000..c859d8f --- /dev/null +++ b/assets/js/gallery.js @@ -0,0 +1,270 @@ +import { BrowserVerifier, prepareVerifier } from '../../verifier/client.mjs'; + +let preparationError; +try { await prepareVerifier(); } catch (error) { preparationError = error.message; } + +(function () { + const $ = (id) => document.getElementById(id); + const root = $('ljGallery'); + if (!root) return; + + const verifier = new BrowserVerifier(); + let renderToken = 0; + let files; + const state = { + examples: [], + activeId: null, + activeTab: 'spec', + complexity: 'all', + factors: new Set(), + mermaidReady: false, + runToken: 0, + }; + + const fileFor = (tab) => ({ + spec: 'spec.java', + correct: 'correct.java', + incorrect: 'incorrect.java', + }[tab]); + + async function fetchText(path) { + const r = await fetch(path, { cache: 'no-cache' }); + if (!r.ok) throw new Error(path + ' -> ' + r.status); + return r.text(); + } + + function passesFilter(ex) { + if (state.complexity !== 'all' && ex.complexity !== state.complexity) return false; + for (const f of state.factors) if (!ex.factors.includes(f)) return false; + return true; + } + + function renderList() { + const list = $('ljList'); + list.innerHTML = ''; + const visible = state.examples.filter(passesFilter); + $('ljCount').textContent = + visible.length + ' of ' + state.examples.length + ' examples'; + for (const ex of visible) { + const li = document.createElement('li'); + li.className = 'lj-item' + (ex.id === state.activeId ? ' lj-item--active' : ''); + li.dataset.id = ex.id; + li.innerHTML = + '' + ex.title + '' + + '' + ex.className + '' + + '' + ex.complexity + ''; + li.addEventListener('click', () => selectExample(ex.id)); + list.appendChild(li); + } + if (visible.length && !visible.some(e => e.id === state.activeId)) { + selectExample(visible[0].id); + } + } + + function resetVerification() { + state.runToken++; + if (verifier.pending) verifier.cancel(); + files = undefined; + $('ljRun').disabled = true; + $('ljRun').textContent = '▶ Run verifier'; + $('ljVerifier').dataset.state = 'spec'; + $('ljVerifierBody').textContent = 'Loading example…'; + } + + function showResult(result) { + $('ljVerifier').dataset.state = result.status === 'success' ? 'ok' : 'err'; + const body = $('ljVerifierBody'); + body.replaceChildren(); + for (const diagnostic of result.diagnostics) { + const paragraph = document.createElement('p'); + const title = document.createElement('strong'); + title.textContent = diagnostic.title; + paragraph.append(title, document.createElement('br'), document.createTextNode(diagnostic.message)); + body.append(paragraph); + } + } + + async function renderDetail() { + const ex = state.examples.find(e => e.id === state.activeId); + if (!ex) return; + $('ljClass').textContent = ex.className; + $('ljTitle').textContent = ex.title; + $('ljBlurb').textContent = ex.blurb; + $('ljMeta').innerHTML = + '' + ex.complexity + '' + + ex.factors.map(f => '' + f + '').join(''); + renderTab(); + const host = $('ljMermaid'); + host.replaceChildren(); + try { + const mer = await fetchText('assets/examples/data/' + ex.id + '/state.mmd'); + if (ex.id !== state.activeId) return; + if (state.mermaidReady && window.mermaid) { + const { svg } = await window.mermaid.render('ljMermaidGraph_' + Date.now(), mer); + if (ex.id === state.activeId) host.innerHTML = svg; + } else host.textContent = mer; + } catch { + if (ex.id === state.activeId) host.textContent = 'Diagram unavailable.'; + } + } + + async function renderTab() { + const token = ++renderToken; + resetVerification(); + const ex = state.examples.find(e => e.id === state.activeId); + const tab = state.activeTab; + try { + const [spec, code] = await Promise.all([ + fetchText('assets/examples/data/' + ex.id + '/spec.java'), + fetchText('assets/examples/data/' + ex.id + '/' + fileFor(tab)) + ]); + if (token !== renderToken) return; + const codeEl = $('ljCode'); + codeEl.className = 'language-java'; + codeEl.textContent = code; + window.Prism?.highlightElement(codeEl); + const specName = spec.match(/(?:class|interface)\s+(\w+)/)[1] + '.java'; + files = { [specName]: spec }; + if (tab !== 'spec') files['Example.java'] = code; + $('ljRun').disabled = false; + $('ljVerifierBody').textContent = tab === 'spec' + ? 'Check this specification, or select a usage to verify its calls.' + : 'Run the verifier to check this usage against its specification.'; + } catch (error) { + if (token !== renderToken) return; + showResult({ status: 'failure', diagnostics: [{ title: 'Example could not load', message: error.message }] }); + } + } + + async function runVerifier() { + if (verifier.pending) { + state.runToken++; + verifier.cancel(); + $('ljRun').textContent = '▶ Run verifier'; + $('ljVerifier').dataset.state = 'spec'; + $('ljVerifierBody').textContent = 'Verification stopped.'; + return; + } + if (!files) return; + const token = ++state.runToken; + $('ljRun').textContent = '■ Stop'; + $('ljVerifier').dataset.state = 'spec'; + try { + if (preparationError) throw new Error(preparationError); + const result = await verifier.verify(files, message => { + if (token === state.runToken) $('ljVerifierBody').textContent = message; + }); + if (token === state.runToken) showResult(result); + } catch (error) { + if (token === state.runToken && error.name !== 'AbortError') { + showResult({ status: 'failure', diagnostics: [{ title: 'Verification could not complete', message: error.message }] }); + } + } finally { + if (token === state.runToken) $('ljRun').textContent = '▶ Run verifier'; + } + } + + function selectExample(id) { + state.activeId = id; + // update list active state + for (const li of document.querySelectorAll('#ljList .lj-item')) { + li.classList.toggle('lj-item--active', li.dataset.id === id); + } + renderDetail(); + } + + function selectTab(tab) { + state.activeTab = tab; + for (const btn of document.querySelectorAll('.lj-tab')) { + const isActive = btn.dataset.tab === tab; + btn.classList.toggle('lj-tab--active', isActive); + btn.setAttribute('aria-selected', isActive ? 'true' : 'false'); + } + renderTab(); + } + + function wireFilters() { + for (const group of document.querySelectorAll('.lj-filters')) { + const kind = group.dataset.group; + for (const chip of group.querySelectorAll('.lj-chip')) { + chip.addEventListener('click', () => { + const v = chip.dataset.value; + if (kind === 'complexity') { + state.complexity = v; + for (const c of group.querySelectorAll('.lj-chip')) + c.classList.toggle('lj-chip--active', c === chip); + } else { + if (state.factors.has(v)) state.factors.delete(v); + else state.factors.add(v); + chip.classList.toggle('lj-chip--active', state.factors.has(v)); + } + renderList(); + }); + } + } + } + + function wireTabs() { + for (const btn of document.querySelectorAll('.lj-tab')) { + btn.addEventListener('click', () => selectTab(btn.dataset.tab)); + } + $('ljRun').addEventListener('click', runVerifier); + } + + async function init() { + try { + state.examples = await (await fetch('assets/examples/examples.json', { cache: 'no-cache' })).json(); + } catch (e) { + root.innerHTML = '

Could not load examples.

'; + return; + } + if (window.mermaid) { + window.mermaid.initialize({ + startOnLoad: false, + theme: 'base', + themeVariables: { + primaryColor: '#ffe7ee', + primaryTextColor: '#212529', + primaryBorderColor: '#cf0e4e', + lineColor: '#cf0e4e', + fontFamily: 'Nunito, system-ui, sans-serif', + fontSize: '14px', + }, + flowchart: { htmlLabels: true }, + }); + state.mermaidReady = true; + } else { + // mermaid loads with `defer`; poll briefly + const start = Date.now(); + while (!window.mermaid && Date.now() - start < 3000) { + await new Promise(r => setTimeout(r, 50)); + } + if (window.mermaid) { + window.mermaid.initialize({ + startOnLoad: false, + theme: 'base', + themeVariables: { + primaryColor: '#fff7ec', + primaryTextColor: '#1a1a2e', + primaryBorderColor: '#1a1a2e', + lineColor: '#1a1a2e', + fontFamily: 'JetBrains Mono, monospace', + fontSize: '14px', + }, + }); + state.mermaidReady = true; + } + } + wireFilters(); + wireTabs(); + state.activeId = state.examples[0].id; + renderList(); + renderDetail(); + } + + if (document.readyState === 'loading') { + document.addEventListener('DOMContentLoaded', init); + } else { + init(); + } + })(); diff --git a/index.html b/index.html index ebf4f00..bda985b 100644 --- a/index.html +++ b/index.html @@ -101,9 +101,11 @@

Extending Java with
Liquid Types

-
- -
+ + + Watch the LiquidJava introduction + See refinements in action on YouTube. +



@@ -523,12 +525,12 @@
-
+
verifier - +
- 

+            

           

         
       

@@ -603,246 +605,7 @@ 

       document.getElementById('year').textContent = new Date().getFullYear();
   
 
-  
-  
+