added refinements and a test file for PipedWriter

JonathanAldrich · JonathanAldrich · commit 8cd62580890b · 2025-12-22T12:31:58.000-05:00
diff --git a/examples/demo/src/main/java/com/example/pipedwriter/PipedWriterRefinements.java 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
@@ -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();
+    }
+}
