Added PipedOutputStream example

pcanelas · pcanelas · commit 9bc3ef7bfd2b · 2025-12-11T17:25:57.000Z
diff --git a/examples/demo/src/main/java/com/barista/pipedoutputstream/PipedOutputStreamMainTest.java b/examples/demo/src/main/java/com/barista/pipedoutputstream/PipedOutputStreamMainTest.java
@@ -0,0 +1,50 @@
+package com.barista.pipedoutputstream;
+
+import java.io.IOException;
+import java.io.PipedInputStream;
+import java.io.PipedOutputStream;
+
+public class PipedOutputStreamMainTest {
+    public static void main(String[] args) throws IOException{
+        //test1();
+        //test2();
+        //test3();
+        //test4();
+        //test5();
+    }
+
+    public static void test1() throws IOException {
+        PipedOutputStream pos = new PipedOutputStream(new PipedInputStream());
+        // I cannot connect if PipedInputStream is provided.
+        pos.connect(null);
+    }
+
+    public static void test2() throws IOException {
+        PipedOutputStream pos = new PipedOutputStream(new PipedInputStream());
+        pos.close();
+        pos.flush();
+    }
+
+    public static void test3() throws IOException {
+        PipedOutputStream pos = new PipedOutputStream(new PipedInputStream());
+        pos.close();
+        // I cannot write a bit after close.
+        pos.write(1);
+    }
+
+    public static void test4() throws IOException {
+        PipedOutputStream pos = new PipedOutputStream(new PipedInputStream());
+        pos.close();
+        byte[] x = {1, 2, 3};
+        // I cannot write bits, offsent, and len after close.
+        pos.write(x, 2, 3);
+    }
+
+    public static void test5() throws IOException {
+        PipedOutputStream pos = new PipedOutputStream(new PipedInputStream());
+        byte[] x = {1, 2, 3};
+        // I cannot have negative values for arguments.
+        pos.write(x, -2, -3);
+        pos.close();
+    }
+}
diff --git a/examples/demo/src/main/java/com/barista/pipedoutputstream/PipedOutputStreamRefinements.java b/examples/demo/src/main/java/com/barista/pipedoutputstream/PipedOutputStreamRefinements.java
@@ -0,0 +1,36 @@
+package com.barista.pipedoutputstream;
+
+import java.io.PipedInputStream;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.Refinement;
+import liquidjava.specification.RefinementAlias;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@RefinementAlias("Nat(int x) {x >= 0}")
+@StateSet({"connected", "created", "closed"})
+@ExternalRefinementsFor("java.io.PipedOutputStream")
+public interface PipedOutputStreamRefinements {
+    
+    @StateRefinement(to="connected(this)")
+    public void PipedOutputStream(PipedInputStream snk);
+
+    @StateRefinement(to="created(this)")
+    public void PipedOutputStream();
+
+    @StateRefinement(from="created(this) || closed(this)", to="connected(this)")
+    public void connect(PipedInputStream snk);
+
+    @StateRefinement(from="connected(this)", to="connected(this)")
+    public void write(int b);
+
+    @StateRefinement(from="connected(this)", to="connected(this)")
+    public void write(byte[] b, @Refinement("Nat(_)") int off, @Refinement("Nat(_)") int len);
+
+    // Testing the execution, I can do flush, no exceptions are raised.
+    public void flush();
+
+    @StateRefinement(from="created(this) || connected(this)", to="closed(this)")
+    public void close();
+}
