diff --git a/examples/demo/src/main/java/com/barista/bufferedinputstream/BufferedInputStreamRefinements.java b/examples/demo/src/main/java/com/barista/bufferedinputstream/BufferedInputStreamRefinements.java new file mode 100644 index 0000000..78c47c8 --- /dev/null +++ b/examples/demo/src/main/java/com/barista/bufferedinputstream/BufferedInputStreamRefinements.java @@ -0,0 +1,54 @@ +package com.barista.bufferedinputstream; + +import java.io.InputStream; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.Refinement; +import liquidjava.specification.RefinementAlias; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@RefinementAlias("Positive(int x) {x >= 0}") +@StateSet({"open", "closed", "marked"}) +@ExternalRefinementsFor("java.io.BufferedInputStream") +public interface BufferedInputStreamRefinements { + + @StateRefinement(to="open(this)") + public void BufferedInputStream(InputStream in); + + @StateRefinement(to="open(this)") + public void BufferedInputStream(InputStream in, @Refinement("Positive(_)") int size); + + @StateRefinement(from="open(this)", to="open(this)") + @StateRefinement(from="marked(this)", to="marked(this)") + public int read(); + + @StateRefinement(from="open(this)", to="open(this)") + @StateRefinement(from="marked(this)", to="marked(this)") + public int read(byte[] b, + @Refinement("Positive(_)") int off, + @Refinement("Positive(_)") int len); + + @StateRefinement(from="open(this)", to="open(this)") + @StateRefinement(from="marked(this)", to="marked(this)") + public long skip(@Refinement("Positive(_)") long n); + + @StateRefinement(from="open(this)", to="open(this)") + @StateRefinement(from="marked(this)", to="marked(this)") + public int available(); + + @StateRefinement(from="open(this)", to="marked(this)") + @StateRefinement(from="marked(this)", to="marked(this)") + public void mark(@Refinement("Positive(_)") int readlimit); + + @StateRefinement(from="marked(this)", to="marked(this)") + public void reset(); + + @StateRefinement(from="open(this)", to="open(this)") + @StateRefinement(from="marked(this)", to="marked(this)") + public boolean markSupported(); + + @StateRefinement(from="open(this)", to="closed(this)") + @StateRefinement(from="marked(this)", to="closed(this)") + public void close(); +} diff --git a/examples/demo/src/main/java/com/barista/bufferedinputstream/BufferedInputStreamTest.java b/examples/demo/src/main/java/com/barista/bufferedinputstream/BufferedInputStreamTest.java new file mode 100644 index 0000000..3254c62 --- /dev/null +++ b/examples/demo/src/main/java/com/barista/bufferedinputstream/BufferedInputStreamTest.java @@ -0,0 +1,12 @@ +package com.barista.bufferedinputstream; + +import java.io.BufferedInputStream; +import java.io.IOException; + +public class BufferedInputStreamTest { + public void test1() throws IOException { + BufferedInputStream x = new BufferedInputStream(null); + x.close(); + x.available(); + } +} diff --git a/examples/demo/src/main/java/com/barista/choicecallback/ChoiceCallbackRefinements.java b/examples/demo/src/main/java/com/barista/choicecallback/ChoiceCallbackRefinements.java new file mode 100644 index 0000000..c09eae4 --- /dev/null +++ b/examples/demo/src/main/java/com/barista/choicecallback/ChoiceCallbackRefinements.java @@ -0,0 +1,17 @@ +package com.barista.choicecallback; + + +import liquidjava.specification.StateSet; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.ExternalRefinementsFor; + +@StateSet({"singleSelection", "multiSelection",}) +@ExternalRefinementsFor("javax.security.auth.callback.ChoiceCallback") +public interface ChoiceCallbackRefinements { + + @StateRefinement(to="!multipleSelectionsAllowed --> singleSelection(this) && multipleSelectionsAllowed --> multiSelection(this)") + public void ChoiceCallback(String prompt, String[] choices, int defaultChoice, boolean multipleSelectionsAllowed); + + @StateRefinement(from="multiSelection(this)", to="multiSelection(this)") + public void setSelectedIndexes(int[] selections); +} diff --git a/examples/demo/src/main/java/com/barista/choicecallback/ChoiceCallbackTest.java b/examples/demo/src/main/java/com/barista/choicecallback/ChoiceCallbackTest.java new file mode 100644 index 0000000..667a87d --- /dev/null +++ b/examples/demo/src/main/java/com/barista/choicecallback/ChoiceCallbackTest.java @@ -0,0 +1,14 @@ +package com.barista.choicecallback; + +import javax.security.auth.callback.ChoiceCallback; + +public class ChoiceCallbackTest { + public void test1() { + ChoiceCallback x = new ChoiceCallback(null, null, 0, true); + x.setSelectedIndexes(null); + } + public void test2() { + ChoiceCallback x = new ChoiceCallback(null, null, 0, false); + x.setSelectedIndexes(null); + } +} diff --git a/examples/demo/src/main/java/com/barista/deflateroutputstream/DeflaterOutputStreamRefinements.java b/examples/demo/src/main/java/com/barista/deflateroutputstream/DeflaterOutputStreamRefinements.java new file mode 100644 index 0000000..edec376 --- /dev/null +++ b/examples/demo/src/main/java/com/barista/deflateroutputstream/DeflaterOutputStreamRefinements.java @@ -0,0 +1,61 @@ +package com.barista.deflateroutputstream; + +import liquidjava.specification.Refinement; +import liquidjava.specification.RefinementAlias; +import liquidjava.specification.StateSet; +import liquidjava.specification.StateRefinement; + +import java.io.OutputStream; +import java.util.zip.Deflater; + +import liquidjava.specification.ExternalRefinementsFor; + +@StateSet({"open", "closed"}) +@RefinementAlias("Nat(int x) {x > 0}") +@ExternalRefinementsFor("java.util.zip.DeflaterOutputStream") +public interface DeflaterOutputStreamRefinements { + + @StateRefinement(to="open(this)") + public void DeflaterOutputStream(OutputStream out, + Deflater def, + @Refinement("Nat(size)") int size, + boolean syncFlush); + + @StateRefinement(to="open(this)") + public void DeflaterOutputStream(OutputStream out, + Deflater def, + @Refinement("Nat(size)") int size); + + @StateRefinement(to="open(this)") + public void DeflaterOutputStream(OutputStream out, + Deflater def, + boolean syncFlush); + + @StateRefinement(to="open(this)") + public void DeflaterOutputStream(OutputStream out, + Deflater def); + + @StateRefinement(to="open(this)") + public void DeflaterOutputStream(OutputStream out, + boolean syncFlush); + + @StateRefinement(to="open(this)") + public void DeflaterOutputStream(OutputStream out); + + @StateRefinement(from="open(this)", to="open(this)") + public void write(int b); + + @StateRefinement(from="open(this)", to="open(this)") + public void write(byte[] b, + int off, + @Refinement("Nat(len)") int len); + + @StateRefinement(from="open(this)", to="open(this)") + public void finish(); + + @StateRefinement(from="open(this)", to="open(this)") + public void flush(); + + @StateRefinement(from="open(this)", to="closed(this)") + public void close(); +} diff --git a/examples/demo/src/main/java/com/barista/deflateroutputstream/DeflaterOutputStreamTest.java b/examples/demo/src/main/java/com/barista/deflateroutputstream/DeflaterOutputStreamTest.java new file mode 100644 index 0000000..8e4eaf2 --- /dev/null +++ b/examples/demo/src/main/java/com/barista/deflateroutputstream/DeflaterOutputStreamTest.java @@ -0,0 +1,19 @@ +package com.barista.deflateroutputstream; + +import java.io.IOException; +import java.util.zip.DeflaterOutputStream; + +public class DeflaterOutputStreamTest { + public void test1() throws IOException { + DeflaterOutputStream x = new DeflaterOutputStream(null); + x.close(); + x.flush(); + } + + public void test2() throws IOException { + DeflaterOutputStream x = new DeflaterOutputStream(null); + x.write(null, 0, -10); + x.flush(); + x.close(); + } +} diff --git a/examples/demo/src/main/java/com/barista/dragsourcecontext/DragSourceContextRefinements.java b/examples/demo/src/main/java/com/barista/dragsourcecontext/DragSourceContextRefinements.java new file mode 100644 index 0000000..3407ece --- /dev/null +++ b/examples/demo/src/main/java/com/barista/dragsourcecontext/DragSourceContextRefinements.java @@ -0,0 +1,54 @@ +package com.barista.dragsourcecontext; + +import liquidjava.specification.StateSet; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.ExternalRefinementsFor; + +import java.awt.Cursor; +import java.awt.Image; +import java.awt.Point; +import java.awt.datatransfer.Transferable; +import java.awt.dnd.DragSourceListener; +import java.awt.dnd.DragGestureEvent; +import java.awt.dnd.DragSourceDragEvent; +import java.awt.dnd.DragSourceDropEvent; +import java.awt.dnd.DragSourceEvent; + +@StateSet({"withListener", "noListener"}) +@ExternalRefinementsFor("java.awt.dnd.DragSourceContext") +public interface DragSourceContextRefinements { + + // @StateRefinement(to="dsl == null ? withListener(this) : noListener(this)") + @StateRefinement(to="withListener(this)") + public void DragSourceContext(DragGestureEvent trigger, + Cursor dragCursor, + Image dragImage, + Point offset, + Transferable t, + DragSourceListener dsl); + + @StateRefinement(from="noListener(this)", to="withListener(this)") + public void addDragSourceListener(DragSourceListener dsl); + + @StateRefinement(from="withListener(this)", to="noListener(this)") + public void removeDragSourceListener(DragSourceListener dsl); + + // Assumption: we always need listeners to enter drag operations + @StateRefinement(from="withListener(this)", to="withListener(this)") + public void dragEnter(DragSourceDragEvent dsde); + + @StateRefinement(from="withListener(this)", to="withListener(this)") + public void dragOver(DragSourceDragEvent dsde); + + @StateRefinement(from="withListener(this)", to="withListener(this)") + public void dragExit(DragSourceEvent dse); + + @StateRefinement(from="withListener(this)", to="withListener(this)") + public void dropActionChanged(DragSourceDragEvent dsde); + + @StateRefinement(from="withListener(this)", to="withListener(this)") + public void dragDropEnd(DragSourceDropEvent dsde); + + @StateRefinement(from="withListener(this)", to="withListener(this)") + public void dragMouseMoved(DragSourceDragEvent dsde); +} diff --git a/examples/demo/src/main/java/com/barista/dragsourcecontext/DragSourceContextTests.java b/examples/demo/src/main/java/com/barista/dragsourcecontext/DragSourceContextTests.java new file mode 100644 index 0000000..6f8fb86 --- /dev/null +++ b/examples/demo/src/main/java/com/barista/dragsourcecontext/DragSourceContextTests.java @@ -0,0 +1,13 @@ +package com.barista.dragsourcecontext; + +import java.awt.dnd.DragSourceContext; +import java.util.TooManyListenersException; + +public class DragSourceContextTests { + public void test1() throws TooManyListenersException { + DragSourceContext dnd = new DragSourceContext(null, null, null, null, null, null); + dnd.removeDragSourceListener(null); + dnd.dragOver(null); + dnd.addDragSourceListener(dnd); + } +} diff --git a/examples/demo/src/main/java/com/barista/droptarget/DropTargetRefinements.java b/examples/demo/src/main/java/com/barista/droptarget/DropTargetRefinements.java new file mode 100644 index 0000000..16be95d --- /dev/null +++ b/examples/demo/src/main/java/com/barista/droptarget/DropTargetRefinements.java @@ -0,0 +1,74 @@ +package com.barista.droptarget; + +import liquidjava.specification.StateSet; +import liquidjava.specification.StateRefinement; + +import java.awt.Component; +import java.awt.datatransfer.FlavorMap; +import java.awt.dnd.DropTargetDragEvent; +import java.awt.dnd.DropTargetDropEvent; +import java.awt.dnd.DropTargetEvent; +import java.awt.dnd.DropTargetListener; + +import liquidjava.specification.ExternalRefinementsFor; + +@StateSet({"noListenerOrComponent", "withListener", "withComponent", "withListenerAndComponent", "active"}) +@ExternalRefinementsFor("java.awt.dnd.DropTarget") +public interface DropTargetRefinements { + + @StateRefinement(to="act ? active(this) : withListenerAndComponent(this)") + public void DropTarget(Component c, + int ops, + DropTargetListener dtl, + boolean act, + FlavorMap fm + ); + + @StateRefinement(to="act ? active(this) : withListener(this)") + public void DropTarget(Component c, + int ops, + DropTargetListener dtl, + boolean act + ); + + @StateRefinement(to="withListenerAndComponent(this)") + public void DropTarget(Component c, int ops, DropTargetListener dtl); + + @StateRefinement(to="withListenerAndComponent(this)") + public void DropTarget(Component c, DropTargetListener dtl); + + @StateRefinement(to="noListenerOrComponent(this)") + public void DropTarget(); + + @StateRefinement(from="withListener(this)", to="withListenerAndComponent(this)") + @StateRefinement(from="noListenerOrComponent(this)", to="withComponent(this)") + public void setComponent(Component c); + + @StateRefinement(from="noListenerOrComponent(this)", to="withListener(this)") + @StateRefinement(from="withComponent(this)", to="withListener(this)") + public void addDropTargetListener(DropTargetListener dtl); + + @StateRefinement(from="withListenerAndComponent(this)", to="withComponent(this)") + @StateRefinement(from="active(this)", to="withComponent(this)") + @StateRefinement(from="withListener(this)", to="noListenerOrComponent(this)") + public void removeDropTargetListener(DropTargetListener dtl); + + @StateRefinement(from="withListenerAndComponent(this)", to="isActive ? active(this) : withListenerAndComponent(this)") + @StateRefinement(from="active(this)", to="isActive ? active(this) : withListenerAndComponent(this)") + public void setActive(boolean isActive); + + @StateRefinement(from="active(this)", to="active(this)") + public void dragEnter(DropTargetDragEvent dtde); + + @StateRefinement(from="active(this)", to="active(this)") + public void dragOver(DropTargetDragEvent dtde); + + @StateRefinement(from="active(this)", to="active(this)") + public void dropActionChanged(DropTargetDragEvent dtde); + + @StateRefinement(from="active(this)", to="active(this)") + public void dragExit(DropTargetEvent dte); + + @StateRefinement(from="active(this)", to="active(this)") + public void drop(DropTargetDropEvent dtde); +} diff --git a/examples/demo/src/main/java/com/barista/droptarget/DropTargetTest.java b/examples/demo/src/main/java/com/barista/droptarget/DropTargetTest.java new file mode 100644 index 0000000..e8a533b --- /dev/null +++ b/examples/demo/src/main/java/com/barista/droptarget/DropTargetTest.java @@ -0,0 +1,55 @@ +package com.barista.droptarget; + +import java.awt.dnd.DropTarget; +import java.util.TooManyListenersException; + +public class DropTargetTest { + public void test1() { + DropTarget dt = new DropTarget(); + dt.setActive(true); + } + + public void test2() { + DropTarget dt = new DropTarget(null, null); + dt.dragEnter(null); + } + + public void test3() { + DropTarget dt = new DropTarget(null, 1, null, false); + dt.dragEnter(null); + } + + public void test4() { + DropTarget dt = new DropTarget(null, 1, null, true); + dt.dragEnter(null); + } + + public void test5() throws TooManyListenersException { + DropTarget dt = new DropTarget(); + dt.addDropTargetListener(null); + dt.dragEnter(null); + } + + public void test6() throws TooManyListenersException { + DropTarget dt = new DropTarget(); + dt.addDropTargetListener(null); + dt.setActive(false); + dt.dragEnter(null); + } + + public void test7() throws TooManyListenersException { + DropTarget dt = new DropTarget(); + dt.addDropTargetListener(null); + dt.setActive(true); + } + + public void test8() throws TooManyListenersException { + DropTarget dt = new DropTarget(); + dt.addDropTargetListener(null); + dt.setComponent(null); + dt.setActive(true); + dt.dragEnter(null); + dt.setActive(false); + dt.dragEnter(null); + } +} diff --git a/examples/demo/src/main/java/com/barista/imagewriteparam/ImageWriteParamRefinements.java b/examples/demo/src/main/java/com/barista/imagewriteparam/ImageWriteParamRefinements.java new file mode 100644 index 0000000..e8a5271 --- /dev/null +++ b/examples/demo/src/main/java/com/barista/imagewriteparam/ImageWriteParamRefinements.java @@ -0,0 +1,98 @@ +package com.barista.imagewriteparam; + +import java.util.Locale; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.Refinement; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"tiling_disabled", "tiling_default", "tiling_explicit", "tiling_explicit_with_parameters", "tiling_copy_from_metadata"}) +@StateSet({"compression_disabled", "compression_default", "compression_explicit", "compression_copy_from_metadata", "compression_explicit_set"}) +@ExternalRefinementsFor("javax.imageio.ImageWriteParam") +public interface ImageWriteParamRefinements { + + @StateRefinement(to="tiling_copy_from_metadata(this) && compression_copy_from_metadata(this)") + public void ImageWriteParam(Locale locale); + + // @StateRefinement(from="", to="") + // This is always false and is set by the subclasses, so if we want to define state transitions at the subclass level is better. + // there is some sort of dependency of the superclass by the subclass. + // public boolean canWriteTiles(); + + // @StateRefinement(from="", to="") + // This is always false and is set by the subclasses, so if we want to define state transitions at the subclass level is better + // public boolean canOffsetTiles(); + + @StateRefinement(to="mode == 0 ? tiling_disabled(this) : (mode == 1 ? tiling_default(this) : (mode == 2 ? tiling_explicit(this) : tiling_copy_from_metadata(this)))") + public void setTilingMode(@Refinement("0 <= mode && mode <= 3") int mode); + + // @StateRefinement() <- Keeps the same so no need for refinements. + // public int getTilingMode(); + + @StateRefinement(from="tiling_explicit(this)", to="tiling_explicit_with_parameters(this)") + @StateRefinement(from="tiling_explicit_with_parameters(this)", to="tiling_explicit_with_parameters(this)") + // The parameters here depend on the class value canWriteTiles + public void setTiling( + @Refinement("tileWidth >= 0") int tileWidth, + @Refinement("tileHeight >= 0") int tileHeight, + int tileGridXOffset, + int tileGridYOffset); + + @StateRefinement(from="tiling_explicit_with_parameters(this)", to="tiling_explicit(this)") + @StateRefinement(from="tiling_explicit(this)", to="tiling_explicit(this)") + public void unsetTiling(); + + @StateRefinement(from="tiling_explicit_with_parameters(this)", to="tiling_explicit_with_parameters(this)") + public int getTileWidth(); + + @StateRefinement(from="tiling_explicit_with_parameters(this)", to="tiling_explicit_with_parameters(this)") + public int getTileHeight(); + + @StateRefinement(from="tiling_explicit_with_parameters(this)", to="tiling_explicit_with_parameters(this)") + public int getTileGridXOffset(); + + @StateRefinement(from="tiling_explicit_with_parameters(this)", to="tiling_explicit_with_parameters(this)") + public int getTileGridYOffset(); + + // No transitions needed here + // public boolean canWriteProgressive(); + public void setProgressiveMode(@Refinement("0 == mode || mode == 1 || mode == 3") int mode); + // public int getProgressiveMode(); + + // No transitions here + // public boolean canWriteCompressed(); + @StateRefinement(to="mode == 0 ? compression_disabled(this) : (mode == 1 ? compression_default(this) : (mode == 2 ? compression_explicit(this) : compression_copy_from_metadata(this)))") + public void setCompressionMode(@Refinement("0 <= mode && mode <= 3") int mode); + + @StateRefinement(from="compression_explicit(this)", to="compression_explicit_set(this)") + public void setCompressionType(String compressionType); + + @StateRefinement(from="compression_explicit(this)", to="compression_explicit(this)") + @StateRefinement(from="compression_explicit_set(this)", to="compression_explicit_set(this)") + public String getCompressionType(); + + @StateRefinement(from="compression_explicit_set(this)", to="compression_explicit(this)") + public void unsetCompression(); + + @StateRefinement(from="compression_explicit_set(this)", to="compression_explicit_set(this)") + public String getLocalizedCompressionTypeName(); + + @StateRefinement(from="compression_explicit_set(this)", to="compression_explicit_set(this)") + public boolean isCompressionLossless(); + + @StateRefinement(from="compression_explicit_set(this)", to="compression_explicit_set(this)") + public void setCompressionQuality(@Refinement("0.0 <= quality && quality <= 1.0") float quality); + + @StateRefinement(from="compression_explicit_set(this)", to="compression_explicit_set(this)") + public float getCompressionQuality(); + + @StateRefinement(from="compression_explicit_set(this)", to="compression_explicit_set(this)") + public float getBitRate(@Refinement("0.0 <= quality && quality <= 1.0") float quality); + + @StateRefinement(from="compression_explicit_set(this)", to="compression_explicit_set(this)") + public String[] getCompressionQualityDescriptions(); + + @StateRefinement(from="compression_explicit_set(this)", to="compression_explicit_set(this)") + public float[] getCompressionQualityValues(); +} diff --git a/examples/demo/src/main/java/com/barista/imagewriteparam/ImageWriteParamTest.java b/examples/demo/src/main/java/com/barista/imagewriteparam/ImageWriteParamTest.java new file mode 100644 index 0000000..cd9b247 --- /dev/null +++ b/examples/demo/src/main/java/com/barista/imagewriteparam/ImageWriteParamTest.java @@ -0,0 +1,32 @@ +package com.barista.imagewriteparam; + +import javax.imageio.ImageWriteParam; + +public class ImageWriteParamTest { + public void test1() { + ImageWriteParam iwp = new ImageWriteParam(null); + iwp.setTilingMode(1); + iwp.setTiling(0, 0, 0, 0); + } + + public void test2() { + ImageWriteParam iwp = new ImageWriteParam(null); + iwp.setTilingMode(2); + iwp.getTileWidth(); + iwp.setTiling(0, 0, 0, 0); + } + + public void test3() { + ImageWriteParam iwp = new ImageWriteParam(null); + iwp.setTilingMode(2); + iwp.setTiling(0, 0, 0, 0); + iwp.unsetTiling(); + iwp.getTileWidth(); + } + + public void test4() { + ImageWriteParam iwp = new ImageWriteParam(null); + iwp.setCompressionMode(2); + iwp.unsetCompression(); + } +} diff --git a/examples/demo/src/main/java/com/barista/logincontext/LoginContextRefinements.java b/examples/demo/src/main/java/com/barista/logincontext/LoginContextRefinements.java new file mode 100644 index 0000000..1a89c2a --- /dev/null +++ b/examples/demo/src/main/java/com/barista/logincontext/LoginContextRefinements.java @@ -0,0 +1,39 @@ +package com.barista.logincontext; + +import liquidjava.specification.StateSet; +import liquidjava.specification.StateRefinement; + +import javax.security.auth.Subject; +import javax.security.auth.callback.CallbackHandler; +import javax.security.auth.login.Configuration; + +import liquidjava.specification.ExternalRefinementsFor; + +@StateSet({"created", "loggedIn", "authenticated", "loggedOut"}) +@ExternalRefinementsFor("javax.security.auth.login.LoginContext") +public interface LoginContextRefinements { + + @StateRefinement(to="created(this)") + public void LoginContext(String name); + + @StateRefinement(to="created(this)") + public void LoginContext(String name, CallbackHandler callbackHandler); + + @StateRefinement(to="created(this)") + public void LoginContext(String name, Subject subject); + + @StateRefinement(to="created(this)") + public void LoginContext(String name, Subject subject, CallbackHandler callbackHandler); + + @StateRefinement(to="created(this)") + public void LoginContext(String name, Subject subject, CallbackHandler callbackHandler, Configuration config); + + @StateRefinement(from="created(this) || loggedOut(this)", to="loggedIn(this)") + public void login(); + + @StateRefinement(from="authenticated(this) || loggedIn(this)", to="loggedOut(this)") + public void logout(); + + @StateRefinement(from="authenticated(this)", to="authenticated(this)") + public Subject getSubject(); +} diff --git a/examples/demo/src/main/java/com/barista/pipedoutputstream/PipedOutputStreamMainTest.java b/examples/demo/src/main/java/com/barista/pipedoutputstream/PipedOutputStreamMainTest.java new file mode 100644 index 0000000..328b256 --- /dev/null +++ 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 new file mode 100644 index 0000000..d8ab733 --- /dev/null +++ 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(); +} diff --git a/examples/demo/src/main/java/com/barista/serversocket/ServerSocketRefinements.java b/examples/demo/src/main/java/com/barista/serversocket/ServerSocketRefinements.java new file mode 100644 index 0000000..2a6aa13 --- /dev/null +++ b/examples/demo/src/main/java/com/barista/serversocket/ServerSocketRefinements.java @@ -0,0 +1,76 @@ +package com.barista.serversocket; + +import liquidjava.specification.Refinement; +import liquidjava.specification.RefinementAlias; +import liquidjava.specification.StateSet; +import liquidjava.specification.StateRefinement; + +import java.net.InetAddress; +import java.net.ServerSocket; +import java.net.SocketAddress; +import java.net.SocketOption; + +import liquidjava.specification.ExternalRefinementsFor; + +@StateSet({"unconnected", "binded", "connected", "closed"}) +@RefinementAlias("Positive(int x) {x >= 0}") +@ExternalRefinementsFor("java.net.ServerSocket") +public interface ServerSocketRefinements { + + // Constructors + @StateRefinement(to="unconnected(this)") + public void ServerSocket(); + + @StateRefinement(to="binded(this)") + public void ServerSocket(@Refinement("Positive(_)") int port); + + @StateRefinement(to="binded(this)") + public void ServerSocket( + @Refinement("Positive(_)") int port, + @Refinement("Positive(_)") int backlog); + + @StateRefinement(to="connected(this)") + public void ServerSocket( + @Refinement("Positive(_)") int port, + @Refinement("Positive(_)") int backlog, + InetAddress bindAddr); + + // Methods + @StateRefinement(from="unconnected(this)", to="binded(this)") + public void bind(SocketAddress bindpoint); + + @StateRefinement(from="unconnected(this)", to="binded(this)") + public void bind(SocketAddress bindpoint, int backlog); + + @StateRefinement(from="unconnected(this) || connected(this) || binded(this)", to="closed(this)") + public void close(); + + @StateRefinement(from="unconnected(this)", to="unconnected(this)") + @StateRefinement(from="binded(this)", to="binded(this)") + @StateRefinement(from="connected(this)", to="connected(this)") + public void setSoTimeout(@Refinement("Positive(_)") int timeout); + + @StateRefinement(from="unconnected(this)", to="unconnected(this)") + @StateRefinement(from="binded(this)", to="binded(this)") + @StateRefinement(from="connected(this)", to="connected(this)") + public void setReuseAddress(boolean on); + + @StateRefinement(from="unconnected(this)", to="unconnected(this)") + @StateRefinement(from="binded(this)", to="binded(this)") + public void setPerformancePreferences(int connectionTime, int latency, int bandwith); + + @StateRefinement(from="unconnected(this)", to="unconnected(this)") + @StateRefinement(from="binded(this)", to="binded(this)") + @StateRefinement(from="connected(this)", to="connected(this)") + public ServerSocket setOption(SocketOption name, T value); + + @StateRefinement(from="unconnected(this)", to="unconnected(this)") + @StateRefinement(from="binded(this)", to="binded(this)") + @StateRefinement(from="connected(this)", to="connected(this)") + public T getOption(SocketOption name); + + @StateRefinement(from="binded(this)", to="binded(this)") + @StateRefinement(from="unconnected(this)", to="unconnected(this)") + @StateRefinement(from="!(size >= 64000) && connected(this)", to="connected(this)") + public void setReceiveBufferSize(int size); +} diff --git a/examples/demo/src/main/java/com/barista/serversocket/ServerSocketTests.java b/examples/demo/src/main/java/com/barista/serversocket/ServerSocketTests.java new file mode 100644 index 0000000..de277f5 --- /dev/null +++ b/examples/demo/src/main/java/com/barista/serversocket/ServerSocketTests.java @@ -0,0 +1,27 @@ +package com.barista.serversocket; + +import java.io.IOException; +import java.net.ServerSocket; + +public class ServerSocketTests { + + + public static void test1() throws IOException { + ServerSocket s = new ServerSocket(); + s.close(); + s.bind(null); + } + + public static void test2() throws IOException { + ServerSocket s = new ServerSocket(8080); + s.bind(null); + } + + public static void test3() throws IOException { + ServerSocket s = new ServerSocket(); + s.bind(null); + s.bind(null); + } + + +} diff --git a/examples/demo/src/main/java/com/barista/socket/SocketRefinements.java b/examples/demo/src/main/java/com/barista/socket/SocketRefinements.java new file mode 100644 index 0000000..0977f1f --- /dev/null +++ b/examples/demo/src/main/java/com/barista/socket/SocketRefinements.java @@ -0,0 +1,83 @@ +package com.barista.socket; + +import java.io.InputStream; +import java.io.OutputStream; +import java.net.InetAddress; +import java.net.Proxy; +import java.net.Socket; +import java.net.SocketAddress; +import java.net.SocketOption; + +import liquidjava.specification.Refinement; +import liquidjava.specification.RefinementAlias; +import liquidjava.specification.StateSet; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.ExternalRefinementsFor; + +@StateSet({"unconnected", "binded", "connected", "closed"}) +@RefinementAlias("Positive(int x) {x >= 0}") +@ExternalRefinementsFor("java.net.Socket") +public interface SocketRefinements { + + // Constructors + @StateRefinement(to="unconnected(this)") + public void Socket(); + + @StateRefinement(to="unconnected(this)") + public void Socket(Proxy proxy); + + @StateRefinement(to="connected(this)") + public void Socket(String host, @Refinement("Positive(_)") int port); + + @StateRefinement(to="connected(this)") + public void Socket(String host, @Refinement("Positive(_)") int port, InetAddress localAddr, @Refinement("Positive(_)") int localPort); + + @StateRefinement(to="connected(this)") + public void Socket(InetAddress address, @Refinement("Positive(_)") int port, InetAddress localAddr, @Refinement("Positive(_)") int localPort); + + // Methods + @StateRefinement(from="unconnected(this)", to="binded(this)") + public void bind(SocketAddress bindpoint); + + @StateRefinement(from="unconnected(this)", to="unconnected(this)") + @StateRefinement(from="binded(this)", to="binded(this)") + public void setPerformancePreferences(int connectionTime, int latency, int bandwith); + + @StateRefinement(from="unconnected(this)", to="unconnected(this)") + @StateRefinement(from="binded(this)", to="binded(this)") + @StateRefinement(from="connected(this)", to="connected(this)") + public Socket setOption(SocketOption name, T value); + + @StateRefinement(from="unconnected(this)", to="unconnected(this)") + @StateRefinement(from="binded(this)", to="binded(this)") + @StateRefinement(from="connected(this)", to="connected(this)") + public T getOption(SocketOption name); + + @StateRefinement(from="connected(this)", to="connected(this)") + public InputStream getInputStream(); + + @StateRefinement(from="connected(this)", to="connected(this)") + public OutputStream getOutputStream(); + + @StateRefinement(from="connected(this)", to="connected(this)") + public void sendUrgentData(int data); + + @StateRefinement(from="unconnected(this) || binded(this)", to="connected(this)") + public void connect(SocketAddress endpoint); + + @StateRefinement(from="unconnected(this) || binded(this)", to="connected(this)") + public void connect(SocketAddress endpoint, @Refinement("Positive(_)") int timeout); + + @StateRefinement(from="binded(this)", to="binded(this)") + @StateRefinement(from="unconnected(this)", to="unconnected(this)") + @StateRefinement(from="!(size >= 64000) && connected(this)", to="connected(this)") + public void setReceiveBufferSize(int size); + + @StateRefinement(from="unconnected(this)", to="unconnected(this)") + @StateRefinement(from="binded(this)", to="binded(this)") + @StateRefinement(from="connected(this)", to="connected(this)") + public void setSoLinger(boolean on, @Refinement("Positive(_)") int linger); + + @StateRefinement(from="unconnected(this) || connected(this) || binded(this)", to="closed(this)") + public void close(); +} diff --git a/examples/demo/src/main/java/com/barista/socket/SocketTest.java b/examples/demo/src/main/java/com/barista/socket/SocketTest.java new file mode 100644 index 0000000..0b8965d --- /dev/null +++ b/examples/demo/src/main/java/com/barista/socket/SocketTest.java @@ -0,0 +1,48 @@ +package com.barista.socket; + +import java.io.IOException; +import java.net.Socket; + +public interface SocketTest { + + public static void test1() throws IOException { + Socket s = new Socket(); + s.close(); + s.sendUrgentData(0); + } + + public static void test2() throws IOException { + Socket s = new Socket("localhost", 8080); + s.bind(null); + } + + + public static void test3() throws IOException { + Socket s = new Socket(); + s.connect(null); + s.connect(null); + } + + public static void test4() throws IOException { + Socket s = new Socket(); + s.bind(null); + s.bind(null); + } + + public static void test5() throws IOException { + Socket s = new Socket(); + s.setReceiveBufferSize(65000); + s.setReceiveBufferSize(650); + + + Socket s2 = new Socket(); + s2.bind(null); + s2.setReceiveBufferSize(65000); + s2.setReceiveBufferSize(650); + + + Socket s3 = new Socket("x", 8080); + s2.setReceiveBufferSize(65000); + s2.setReceiveBufferSize(650); + } +} diff --git a/examples/demo/src/main/java/com/barista/throwable/ThrowableRefinements.java b/examples/demo/src/main/java/com/barista/throwable/ThrowableRefinements.java new file mode 100644 index 0000000..4fa4acf --- /dev/null +++ b/examples/demo/src/main/java/com/barista/throwable/ThrowableRefinements.java @@ -0,0 +1,28 @@ +package com.barista.throwable; + +import liquidjava.specification.StateSet; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.ExternalRefinementsFor; + +@StateSet({"withThrowable", "noThrowable"}) +@ExternalRefinementsFor("java.lang.Throwable") +public interface ThrowableRefinements { + + @StateRefinement(to="noThrowable(this)") + public void Throwable(); + + @StateRefinement(to="noThrowable(this)") + public void Throwable(String message); + + @StateRefinement(to="withThrowable(this)") + public void Throwable(String message, Throwable cause); + + @StateRefinement(to="withThrowable(this)") + public void Throwable(Throwable cause); + + @StateRefinement(to="withThrowable(this)") + public void Throwable(String message, Throwable cause, boolean enableSuppression, boolean writableStackTrace); + + @StateRefinement(from="noThrowable(this)", to="withThrowable(this)") + public Throwable initCause(Throwable cause); +} diff --git a/examples/demo/src/main/java/com/barista/throwable/ThrowableTest.java b/examples/demo/src/main/java/com/barista/throwable/ThrowableTest.java new file mode 100644 index 0000000..414868c --- /dev/null +++ b/examples/demo/src/main/java/com/barista/throwable/ThrowableTest.java @@ -0,0 +1,17 @@ +package com.barista.throwable; + +import java.lang.Throwable; + +public class ThrowableTest { + public void test1() { + Throwable x = new Throwable(); + x.initCause(x); + x.initCause(x); + } + + public void test2() { + Throwable x = new Throwable(); + Throwable y = new Throwable(x); + x.initCause(y); + } +} diff --git a/examples/demo/src/main/java/com/barista/timer/TimerRefinements.java b/examples/demo/src/main/java/com/barista/timer/TimerRefinements.java new file mode 100644 index 0000000..2926dbe --- /dev/null +++ b/examples/demo/src/main/java/com/barista/timer/TimerRefinements.java @@ -0,0 +1,57 @@ +package com.barista.timer; + +import java.util.Date; +import java.util.TimerTask; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.Refinement; +import liquidjava.specification.RefinementAlias; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"created", "scheduled", "canceled"}) +@RefinementAlias("Period(int x) {_ > 0}") +@RefinementAlias("Delay(int x) {_ >= 0}") +@ExternalRefinementsFor("java.util.Timer") +public interface TimerRefinements { + + @StateRefinement(to="created(this)") + public void Timer(); + + @StateRefinement(to="created(this)") + public void Timer(String name); + + @StateRefinement(to="created(this)") + public void Timer(String name, boolean isDaemon); + + @StateRefinement(from="created(this) || canceled(this) || scheduled(this)", to="scheduled(this)") + public void schedule(TimerTask task, @Refinement("Delay(_)") long delay); + + @StateRefinement(from="created(this) || canceled(this) || scheduled(this)", to="scheduled(this)") + public void schedule(TimerTask task, Date time); + + @StateRefinement(from="created(this) || canceled(this) || scheduled(this)", to="scheduled(this)") + public void schedule(TimerTask task, + @Refinement("Delay(_)") long delay, + @Refinement("Period(_)")long period); + + + @StateRefinement(from="created(this) || canceled(this) || scheduled(this)", to="scheduled(this)") + public void schedule(TimerTask task, Date time, + @Refinement("Period(_)")long period); + + @StateRefinement(from="created(this) || canceled(this) || scheduled(this)", to="scheduled(this)") + public void scheduleAtFixedRate(TimerTask task, + @Refinement("Delay(_)") long delay, + @Refinement("Period(_)")long period); + + @StateRefinement(from="created(this) || canceled(this) || scheduled(this)", to="scheduled(this)") + public void scheduleAtFixedRate(TimerTask task, Date time, + @Refinement("Period(_)")long period); + + @StateRefinement(from="created(this) || canceled(this) || scheduled(this)", to="canceled(this)") + public void cancel(); + + // Keeps the same state, nothing changes + public void purge(); +} diff --git a/examples/demo/src/main/java/com/barista/timer/TimerTest.java b/examples/demo/src/main/java/com/barista/timer/TimerTest.java new file mode 100644 index 0000000..682871d --- /dev/null +++ b/examples/demo/src/main/java/com/barista/timer/TimerTest.java @@ -0,0 +1,23 @@ +package com.barista.timer; + +import java.util.Timer; + +public class TimerTest { + public static void main(String[] args) { + //test1(); + //test2(); + //test3(); + //test4(); + //test5(); + } + + public static void test1() { + Timer t = new Timer(); + t.schedule(null, -1); + } + + public static void test2() { + Timer t = new Timer(); + t.schedule(null, 1, 0); + } +} diff --git a/examples/demo/src/main/java/com/barista/xmlfilterimpl/XMLFilterImplRefinements.java b/examples/demo/src/main/java/com/barista/xmlfilterimpl/XMLFilterImplRefinements.java new file mode 100644 index 0000000..c164e9a --- /dev/null +++ b/examples/demo/src/main/java/com/barista/xmlfilterimpl/XMLFilterImplRefinements.java @@ -0,0 +1,41 @@ +package com.barista.xmlfilterimpl; + +import org.xml.sax.InputSource; +import org.xml.sax.XMLReader; + +import liquidjava.specification.StateSet; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.ExternalRefinementsFor; + +@StateSet({"parentless", "withparent"}) +@ExternalRefinementsFor("org.xml.sax.helpers.XMLFilterImpl") +public interface XMLFilterImplRefinements { + // Constructors + @StateRefinement(to="parentless(this)") + public void XMLFilterImpl(); + + @StateRefinement(to="withparent(this)") + public void XMLFilterImpl(XMLReader parent); + + // Methods + @StateRefinement(from="parentless(this) || withparent(this)", to="withparent(this)") + public void setParent(XMLReader parent); + + @StateRefinement(from="withparent(this)", to="withparent(this)") + public void setProperty(String name, Object value); + + @StateRefinement(from="withparent(this)", to="withparent(this)") + public Object getProperty(String name); + + @StateRefinement(from="withparent(this)", to="withparent(this)") + public void setFeature(String name, boolean value); + + @StateRefinement(from="withparent(this)", to="withparent(this)") + public boolean getFeature(String name); + + @StateRefinement(from="withparent(this)", to="withparent(this)") + public void parse(InputSource input); + + @StateRefinement(from="withparent(this)", to="withparent(this)") + public void parse(String systemId); +} diff --git a/examples/demo/src/main/java/com/barista/xmlfilterimpl/XMLFilterImplTest.java b/examples/demo/src/main/java/com/barista/xmlfilterimpl/XMLFilterImplTest.java new file mode 100644 index 0000000..d4d1e91 --- /dev/null +++ b/examples/demo/src/main/java/com/barista/xmlfilterimpl/XMLFilterImplTest.java @@ -0,0 +1,18 @@ +package com.barista.xmlfilterimpl; + +import org.xml.sax.SAXNotRecognizedException; +import org.xml.sax.SAXNotSupportedException; +import org.xml.sax.helpers.XMLFilterImpl; + +public class XMLFilterImplTest { + + public void test1() throws SAXNotRecognizedException, SAXNotSupportedException { + XMLFilterImpl xml = new XMLFilterImpl(); + xml.setProperty("key", null); + } + + public void test2() throws SAXNotRecognizedException, SAXNotSupportedException { + XMLFilterImpl xml = new XMLFilterImpl(null); + xml.setProperty("key", null); + } +}