ZipOutputStream Refinements

rcosta358 · rcosta358 · commit 51589788a86e · 2026-01-13T16:42:32.000Z
diff --git a/examples/demo/src/main/java/com/zipOutputStream/ZipOutputStreamRefinements.java b/examples/demo/src/main/java/com/zipOutputStream/ZipOutputStreamRefinements.java
@@ -0,0 +1,49 @@
+package com.zipOutputStream;
+
+import java.io.IOException;
+import java.io.OutputStream;
+import java.nio.charset.Charset;
+import java.util.zip.ZipEntry;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.Refinement;
+import liquidjava.specification.RefinementAlias;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@RefinementAlias("Positive(int v) { v >= 0 }")
+@RefinementAlias("Level(int v) { 0 <= v && v <= 9 }")
+@StateSet({"open", "ready", "closed"})
+@ExternalRefinementsFor("java.util.zip.ZipOutputStream")
+public interface ZipOutputStreamRefinements {
+    
+    @StateRefinement(to="open(this)")
+    public void ZipOutputStream(OutputStream out);
+
+    @StateRefinement(to="open(this)")
+    public void ZipOutputStream(OutputStream out, Charset charset);
+
+    @StateRefinement(from="open(this)", to="open(this)") 
+    public void setComment(/*@Refinement("'length(_) <= 65535'")*/String comment);
+
+    @StateRefinement(from="open(this)", to="open(this)") 
+    public void setMethod(@Refinement("Positive(_)") int method); // too many different possible values, none of them are negative though
+
+    @StateRefinement(from="open(this)", to="open(this)") 
+    public void setLevel(@Refinement("Level(_)") int level);
+
+    @StateRefinement(from="open(this)", to="ready(this)") 
+    public void putNextEntry(ZipEntry e) throws IOException;
+
+    @StateRefinement(from="ready(this)", to="open(this)") 
+    public void closeEntry() throws IOException;
+    
+    @StateRefinement(from="ready(this)", to="ready(this)") 
+    public void write(byte[] b, @Refinement("Positive(_)") int off, @Refinement("Positive(_)") int len) throws IOException;
+
+    @StateRefinement(from="ready(this)", to="ready(this)") 
+    public void finish() throws IOException;
+
+    @StateRefinement(from="!closed(this)", to="closed(this)") 
+    public void close() throws IOException;
+}
diff --git a/examples/demo/src/main/java/com/zipOutputStream/ZipOutputStreamTests.java b/examples/demo/src/main/java/com/zipOutputStream/ZipOutputStreamTests.java
@@ -0,0 +1,22 @@
+package com.zipOutputStream;
+
+import java.io.FileOutputStream;
+import java.util.zip.ZipOutputStream;
+
+public class ZipOutputStreamTests {
+
+    void testWritingToClosedStream() throws Exception {
+        FileOutputStream fos = new FileOutputStream("file");
+        ZipOutputStream zos = new ZipOutputStream(fos);
+        zos.setMethod(8);
+        zos.setLevel(5);
+        zos.close();
+        zos.write(null, 0, 0);
+    }
+
+    void testParametricRefinements() throws Exception {
+        FileOutputStream fos = new FileOutputStream("file");
+        ZipOutputStream zos = new ZipOutputStream(fos);
+        zos.setLevel(10);
+    }
+}
