From 8cd62580890b890fc60e0d43ec94d7f0476e71da Mon Sep 17 00:00:00 2001 From: Jonathan Aldrich Date: Mon, 22 Dec 2025 12:31:58 -0500 Subject: [PATCH 1/4] added refinements and a test file for PipedWriter --- .../pipedwriter/PipedWriterRefinements.java | 43 +++++++++++++++++++ .../example/pipedwriter/PipedWriterTest.java | 35 +++++++++++++++ 2 files changed, 78 insertions(+) create mode 100644 examples/demo/src/main/java/com/example/pipedwriter/PipedWriterRefinements.java create mode 100644 examples/demo/src/main/java/com/example/pipedwriter/PipedWriterTest.java diff --git a/examples/demo/src/main/java/com/example/pipedwriter/PipedWriterRefinements.java b/examples/demo/src/main/java/com/example/pipedwriter/PipedWriterRefinements.java new file mode 100644 index 0000000..a338ef7 --- /dev/null +++ b/examples/demo/src/main/java/com/example/pipedwriter/PipedWriterRefinements.java @@ -0,0 +1,43 @@ +package com.example.pipedwriter; + +import java.io.IOException; +import java.io.PipedReader; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.Refinement; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@ExternalRefinementsFor("java.io.PipedWriter") +//@RefinementAlias("Index(int x) {x >= 0}") +@StateSet({"unconnected", "connected", "broken", "closed"}) +public interface PipedWriterRefinements { + @StateRefinement(to="connected(this)") + public void PipedWriter(PipedReader snk) + throws IOException; + + @StateRefinement(to="unconnected(this)") + public void PipedWriter(); + + @StateRefinement(from="unconnected(this)", to="connected(this)") + public void connect(PipedReader snk) + throws IOException; + + @StateRefinement(from="connected(this)") + public void write(@Refinement("c >= 0 && c <= 65535") int c) + throws IOException; + + @StateRefinement(from="connected(this)") + public void write(char[] cbuf, + @Refinement("off >= 0") int off, + @Refinement("off >= 0") int len) + throws IOException; + + @StateRefinement(from="connected(this)") + public void flush() + throws IOException; + + @StateRefinement(to="closed(this)") + public void close() + throws IOException; +} diff --git a/examples/demo/src/main/java/com/example/pipedwriter/PipedWriterTest.java b/examples/demo/src/main/java/com/example/pipedwriter/PipedWriterTest.java new file mode 100644 index 0000000..561b17e --- /dev/null +++ b/examples/demo/src/main/java/com/example/pipedwriter/PipedWriterTest.java @@ -0,0 +1,35 @@ +package com.example.pipedwriter; + +import java.io.IOException; +import java.io.PipedReader; +import java.io.PipedWriter; + +public class PipedWriterTest { + void test1() throws IOException { + PipedWriter p = new PipedWriter(); + PipedReader r = new PipedReader(); + p.connect(r); + p.write('a'); + p.flush(); + p.close(); + r.close(); + } + void test2() throws IOException { + PipedReader r = new PipedReader(); + PipedWriter p = new PipedWriter(r); + char [] arr = {'a', 'b', 'c'}; + p.write(arr, 1, 2); + p.flush(); + p.close(); + r.close(); + } + void testFail() throws IOException { + PipedWriter p = new PipedWriter(); + PipedReader r = new PipedReader(); + p.flush(); + char [] arr = {'a', 'b', 'c'}; + p.write(arr, 2, 2); + p.close(); + r.close(); + } +} From 6642faa09cd541f1d8e834609f36300b9c836d27 Mon Sep 17 00:00:00 2001 From: Jonathan Aldrich Date: Mon, 16 Feb 2026 00:44:25 -0500 Subject: [PATCH 2/4] annotations for AbstractUndoableEdit --- .../AbstractUndoableEditRefinements.java | 47 +++++++++++++++++++ .../AbstractUndoableEditTest.java | 31 ++++++++++++ 2 files changed, 78 insertions(+) create mode 100644 examples/demo/src/main/java/com/example/abstractundoableedit/AbstractUndoableEditRefinements.java create mode 100644 examples/demo/src/main/java/com/example/abstractundoableedit/AbstractUndoableEditTest.java diff --git a/examples/demo/src/main/java/com/example/abstractundoableedit/AbstractUndoableEditRefinements.java b/examples/demo/src/main/java/com/example/abstractundoableedit/AbstractUndoableEditRefinements.java new file mode 100644 index 0000000..c8d096d --- /dev/null +++ b/examples/demo/src/main/java/com/example/abstractundoableedit/AbstractUndoableEditRefinements.java @@ -0,0 +1,47 @@ +package com.example.abstractundoableedit; + +import javax.swing.undo.CannotUndoException; +import javax.swing.undo.UndoableEdit; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.Refinement; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@ExternalRefinementsFor("javax.swing.undo.AbstractUndoableEdit") +@StateSet({"alive_done", "not_alive_done", "alive_not_done", "not_alive_not_done"}) +public interface AbstractUndoableEditRefinements { + @StateRefinement(to="alive_done(this)") + public void AbstractUndoableEdit(); + + @StateRefinement(from="alive_done(this)", to="not_alive_done(this)") + @StateRefinement(from="alive_not_done(this)", to="not_alive_not_done(this)") + public void die(); + + + @StateRefinement(from="alive_done(this)", to="alive_not_done(this)") + public void undo() throws CannotUndoException; + + @Refinement("_ && alive_done(this) || !_ && !alive_done(this)") + public boolean canUndo(); + + @StateRefinement(from="alive_not_done(this)", to="alive_done(this)") + public void redo() throws CannotUndoException; + + @Refinement("_ && alive_not_done(this) || !_ && !alive_not_done(this)") + public boolean canRedo(); + + public boolean addEdit(UndoableEdit anEdit); + + public boolean replaceEdit(UndoableEdit anEdit); + + public boolean isSignificant(); + + public String getPresentationName(); + + public String getUndoPresentationName(); + + public String getRedoPresentationName(); + + public String toString(); +} diff --git a/examples/demo/src/main/java/com/example/abstractundoableedit/AbstractUndoableEditTest.java b/examples/demo/src/main/java/com/example/abstractundoableedit/AbstractUndoableEditTest.java new file mode 100644 index 0000000..aa4e8be --- /dev/null +++ b/examples/demo/src/main/java/com/example/abstractundoableedit/AbstractUndoableEditTest.java @@ -0,0 +1,31 @@ +package com.example.abstractundoableedit; + +import javax.swing.undo.AbstractUndoableEdit; + +public class AbstractUndoableEditTest { + void test1() { + AbstractUndoableEdit a = new AbstractUndoableEdit(); + //a.die(); // if commented in, LiquidJava should report an error on the next line + a.undo(); + a.redo(); + a.die(); + } + + void test4() { + AbstractUndoableEdit a = new AbstractUndoableEdit(); + a.undo(); + a.die(); + } + + void test2(AbstractUndoableEdit a) { + if (a.canUndo()) { + a.undo(); + a.redo(); + } + } + void test3(AbstractUndoableEdit a) { + if (a.canRedo()) { + a.redo(); + } + } +} From e35f5ce7e0e19f33be3d3ad6ad716e658a780441 Mon Sep 17 00:00:00 2001 From: Jonathan Aldrich Date: Wed, 18 Feb 2026 14:47:59 -0500 Subject: [PATCH 3/4] update tests so LiquidJava doesn't break (work around char literal bug) --- .../java/com/example/pipedwriter/PipedWriterTest.java | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/examples/demo/src/main/java/com/example/pipedwriter/PipedWriterTest.java b/examples/demo/src/main/java/com/example/pipedwriter/PipedWriterTest.java index 561b17e..669995d 100644 --- a/examples/demo/src/main/java/com/example/pipedwriter/PipedWriterTest.java +++ b/examples/demo/src/main/java/com/example/pipedwriter/PipedWriterTest.java @@ -9,7 +9,7 @@ void test1() throws IOException { PipedWriter p = new PipedWriter(); PipedReader r = new PipedReader(); p.connect(r); - p.write('a'); + p.write(/*'a'*/35); p.flush(); p.close(); r.close(); @@ -17,7 +17,9 @@ void test1() throws IOException { void test2() throws IOException { PipedReader r = new PipedReader(); PipedWriter p = new PipedWriter(r); - char [] arr = {'a', 'b', 'c'}; + char [] arr = {}; // OK for LiquidJava + // char c = 'a'; // breaks LiquidJava + p.write(arr, 1, 2); p.flush(); p.close(); @@ -26,9 +28,10 @@ void test2() throws IOException { void testFail() throws IOException { PipedWriter p = new PipedWriter(); PipedReader r = new PipedReader(); + //char [] arr = {'a', 'b', 'c'}; // breaks LiquidJava p.flush(); - char [] arr = {'a', 'b', 'c'}; - p.write(arr, 2, 2); + char [] arr2 = {'a', 'b', 'c'}; // breaks LiquidJava if analyzed (it isn't here, because there's an error in p.flush() above) + p.write(arr2, 2, 2); p.close(); r.close(); } From 277bc9f11ea4414e67aa0bc530d78fda3a32c45c Mon Sep 17 00:00:00 2001 From: Jonathan Aldrich Date: Wed, 18 Feb 2026 16:04:17 -0500 Subject: [PATCH 4/4] added UUID case study --- .../com/example/uuid/UUIDRefinements.java | 34 +++++++++++++++++++ .../main/java/com/example/uuid/UUIDTest.java | 23 +++++++++++++ 2 files changed, 57 insertions(+) create mode 100644 examples/demo/src/main/java/com/example/uuid/UUIDRefinements.java create mode 100644 examples/demo/src/main/java/com/example/uuid/UUIDTest.java diff --git a/examples/demo/src/main/java/com/example/uuid/UUIDRefinements.java b/examples/demo/src/main/java/com/example/uuid/UUIDRefinements.java new file mode 100644 index 0000000..3b2a6fb --- /dev/null +++ b/examples/demo/src/main/java/com/example/uuid/UUIDRefinements.java @@ -0,0 +1,34 @@ +package com.example.uuid; + +import java.util.UUID; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.Refinement; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@ExternalRefinementsFor("java.util.UUID") +@StateSet({"time_based", "dce_security", "name_based", "random"}) +public interface UUIDRefinements { + //@StateRefinement(from="leastSigBits & 0xC000000000000000 == 0xB000000000000000 && mostSigBits & 0x000000000000F000 == 0x0000000000001000", to="time_based(this)") + public void UUID(long mostSigBits, long leastSigBits); + + // QUESTION: is this how static methods should be specified? + @Refinement("random(_)") + public UUID randomUUID(); + + @Refinement("name_based(_)") + public UUID nameUUIDFromBytes(byte[] name); + + @Refinement("_ == 1 && time_based(this) || _ == 2 && dce_security(this) || _ == 3 && name_based(this) || _ == 4 && random(this)") + public int version(); + + @StateRefinement(from="time_based(this)") + public long timestamp(); + + @StateRefinement(from="time_based(this)") + public int clockSequence(); + + @StateRefinement(from="time_based(this)") + public long node(); +} diff --git a/examples/demo/src/main/java/com/example/uuid/UUIDTest.java b/examples/demo/src/main/java/com/example/uuid/UUIDTest.java new file mode 100644 index 0000000..55b4364 --- /dev/null +++ b/examples/demo/src/main/java/com/example/uuid/UUIDTest.java @@ -0,0 +1,23 @@ +package com.example.uuid; + +import java.util.UUID; + +public class UUIDTest { + void test1fail() { + UUID u = UUID.randomUUID(); + u.timestamp(); // should report an error, because u is not time-based + } + void test2fail(UUID u) { + u.clockSequence(); // should report an error, because u may not be time-based + } + void test3(UUID u) { + if (u.version() == 1) { + u.node(); // should be OK, because u is time-based + } + } + void test4fail(UUID u) { + if (u.version() == 2) { + u.timestamp(); // should report an error, because u is not time-based -- but I don't get an error. + } + } +}