From 517d004e4a2d7f875846cae31d49dd65a77aadb0 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 12 Jan 2026 14:56:10 +0000 Subject: [PATCH 01/11] BufferedReader Refinements --- .../BufferedReaderRefinements.java | 58 +++++++++++++++++++ .../bufferedreader/BufferedReaderTests.java | 35 +++++++++++ .../com/example/ArrayDequeRefinements.java | 38 ------------ .../main/java/com/example/TestArrayDeque.java | 24 -------- .../src/main/java/com/example/TestSimple.java | 17 ------ .../src/test/java/com/example/AppTest.java | 20 ------- 6 files changed, 93 insertions(+), 99 deletions(-) create mode 100644 examples/demo/src/main/java/com/bufferedreader/BufferedReaderRefinements.java create mode 100644 examples/demo/src/main/java/com/bufferedreader/BufferedReaderTests.java delete mode 100644 examples/demo/src/main/java/com/example/ArrayDequeRefinements.java delete mode 100644 examples/demo/src/main/java/com/example/TestArrayDeque.java delete mode 100644 examples/demo/src/main/java/com/example/TestSimple.java delete mode 100644 examples/demo/src/test/java/com/example/AppTest.java diff --git a/examples/demo/src/main/java/com/bufferedreader/BufferedReaderRefinements.java b/examples/demo/src/main/java/com/bufferedreader/BufferedReaderRefinements.java new file mode 100644 index 0000000..5af8070 --- /dev/null +++ b/examples/demo/src/main/java/com/bufferedreader/BufferedReaderRefinements.java @@ -0,0 +1,58 @@ +package com.bufferedreader; + +import java.io.IOException; +import java.io.Reader; +import java.util.stream.Stream; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.Refinement; +import liquidjava.specification.RefinementAlias; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@RefinementAlias("NonNegative(int v) { v >= 0 }") +@RefinementAlias("Positive(int v) { v > 0 }") +@StateSet({"open", "marked", "closed"}) +@ExternalRefinementsFor("java.io.BufferedReader") +public interface BufferedReaderRefinements { + + @StateRefinement(to="open(this)") + public void BufferedReader(Reader in); + + @StateRefinement(to="open(this)") + public void BufferedReader(Reader in, @Refinement("Positive(_)") int sz); + + @StateRefinement(from="open(this)", to="open(this)") + @StateRefinement(from="marked(this)", to="marked(this)") + public int read() throws IOException; + + @StateRefinement(from="open(this)", to="open(this)") + @StateRefinement(from="marked(this)", to="marked(this)") + public int read(char[] cbuf, @Refinement("NonNegative(_)") int off, @Refinement("NonNegative(_)") int len) throws IOException; // cant write "|| len <= cbuf.length - off" + + @StateRefinement(from="open(this)", to="open(this)") + @StateRefinement(from="marked(this)", to="marked(this)") + public String readLine() throws IOException; + + @StateRefinement(from="open(this)", to="open(this)") + @StateRefinement(from="marked(this)", to="marked(this)") + public boolean ready() throws IOException; + + @StateRefinement(from="open(this)", to="open(this)") + @StateRefinement(from="marked(this)", to="marked(this)") + public boolean markSupported(); + + @StateRefinement(from="open(this)", to="marked(this)") + @StateRefinement(from="marked(this)", to="marked(this)") + public void mark(@Refinement("NonNegative(_)") int readAheadLimit) throws IOException; + + @StateRefinement(from="marked(this)", to="open(this)") + public void reset() throws IOException; + + @StateRefinement(from="!closed(this)", to="closed(this)") + public void close() throws IOException; + + @StateRefinement(from="open(this)", to="open(this)") + @StateRefinement(from="marked(this)", to="marked(this)") + public Stream lines(); +} diff --git a/examples/demo/src/main/java/com/bufferedreader/BufferedReaderTests.java b/examples/demo/src/main/java/com/bufferedreader/BufferedReaderTests.java new file mode 100644 index 0000000..6a1f86d --- /dev/null +++ b/examples/demo/src/main/java/com/bufferedreader/BufferedReaderTests.java @@ -0,0 +1,35 @@ +package com.bufferedreader; + +import java.io.BufferedReader; +import java.io.FileReader; + +public class BufferedReaderTests { + + void readClosedFile() throws Exception { + BufferedReader in = new BufferedReader(new FileReader("foo.in")); + in.close(); + in.read(); + } + + void resetUnmarkedFile() throws Exception { + BufferedReader in = new BufferedReader(new FileReader("foo.in")); + in.reset(); + } + + void negativeLength() throws Exception { + BufferedReader in = new BufferedReader(new FileReader("foo.in"), -1); + } + + void noErrors() throws Exception { + BufferedReader in = new BufferedReader(new FileReader("foo.in"), 100); + int bufSize = 10; + char[] buf = new char[bufSize]; + in.ready(); + in.read(); + in.readLine(); + in.mark(10); + in.reset(); + in.read(buf, 0, bufSize); + in.close(); + } +} diff --git a/examples/demo/src/main/java/com/example/ArrayDequeRefinements.java b/examples/demo/src/main/java/com/example/ArrayDequeRefinements.java deleted file mode 100644 index 9ee7b37..0000000 --- a/examples/demo/src/main/java/com/example/ArrayDequeRefinements.java +++ /dev/null @@ -1,38 +0,0 @@ -package com.example; - -import liquidjava.specification.ExternalRefinementsFor; -import liquidjava.specification.Ghost; -import liquidjava.specification.Refinement; -import liquidjava.specification.StateRefinement; - -@ExternalRefinementsFor("java.util.ArrayDeque") -@Ghost("int size") -public interface ArrayDequeRefinements { - - public void ArrayDeque(); - - @StateRefinement(to="size(this) == (size(old(this)) + 1)") - public boolean add(E elem); - - @StateRefinement(to="size(this) == (size(old(this)) + 1)") - public boolean offerFirst(E elem); - - @StateRefinement(from="size(this) > 0", to = "size(this) == (size(old(this)))") - public E getFirst(); - - @StateRefinement(from="size(this) > 0", to = "size(this) == (size(old(this)))") - public E getLast(); - - @StateRefinement(from="size(this)> 0", to="size(this) == (size(old(this)) - 1)") - public void remove(); - - @StateRefinement(from="size(this)> 0", to="size(this) == (size(old(this)) - 1)") - public E pop(); - - @Refinement("_ == size(this)") - public int size(); - - @Refinement("_ == (size(this) <= 0)") - public boolean isEmpty(); - -} diff --git a/examples/demo/src/main/java/com/example/TestArrayDeque.java b/examples/demo/src/main/java/com/example/TestArrayDeque.java deleted file mode 100644 index 155043c..0000000 --- a/examples/demo/src/main/java/com/example/TestArrayDeque.java +++ /dev/null @@ -1,24 +0,0 @@ -package com.example; - -import java.io.IOException; -import java.util.ArrayDeque; - -public class TestArrayDeque { - - public static void main(String[] args) throws IOException{ - /*Uncomment Below*/ - ArrayDeque p = new ArrayDeque<>(); - p.add(2); - p.remove(); - p.offerFirst(6); - p.getLast(); - p.remove(); - // p.getLast(); - p.add(78); - p.add(8); - p.getFirst(); - - - } - -} diff --git a/examples/demo/src/main/java/com/example/TestSimple.java b/examples/demo/src/main/java/com/example/TestSimple.java deleted file mode 100644 index 6b7c371..0000000 --- a/examples/demo/src/main/java/com/example/TestSimple.java +++ /dev/null @@ -1,17 +0,0 @@ -package com.example; -import liquidjava.specification.Refinement; - - -/** - * Hello world! - * - */ -public class TestSimple { - - - public static void main( String[] args ){ - - @Refinement("a > 0") - int a = -1; - } -} diff --git a/examples/demo/src/test/java/com/example/AppTest.java b/examples/demo/src/test/java/com/example/AppTest.java deleted file mode 100644 index 22a94ca..0000000 --- a/examples/demo/src/test/java/com/example/AppTest.java +++ /dev/null @@ -1,20 +0,0 @@ -package com.example; - -import static org.junit.Assert.assertTrue; - -import org.junit.Test; - -/** - * Unit test for simple App. - */ -public class AppTest -{ - /** - * Rigorous Test :-) - */ - @Test - public void shouldAnswerWithTrue() - { - assertTrue( true ); - } -} From 5a4414f7fb84d49dcf8257d361ca594584ec4704 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 13 Jan 2026 16:00:39 +0000 Subject: [PATCH 02/11] ChoiceCallBack Refinements --- .../ChoiceCallbackRefinements.java | 20 +++++++++++++++++++ .../choiceCallback/ChoiceCallbackTests.java | 13 ++++++++++++ 2 files changed, 33 insertions(+) create mode 100644 examples/demo/src/main/java/com/choiceCallback/ChoiceCallbackRefinements.java create mode 100644 examples/demo/src/main/java/com/choiceCallback/ChoiceCallbackTests.java diff --git a/examples/demo/src/main/java/com/choiceCallback/ChoiceCallbackRefinements.java b/examples/demo/src/main/java/com/choiceCallback/ChoiceCallbackRefinements.java new file mode 100644 index 0000000..b588052 --- /dev/null +++ b/examples/demo/src/main/java/com/choiceCallback/ChoiceCallbackRefinements.java @@ -0,0 +1,20 @@ +package com.choiceCallback; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"single", "multiple"}) +@ExternalRefinementsFor("javax.security.auth.callback.ChoiceCallback") +public interface ChoiceCallbackRefinements { + + // not supported + @StateRefinement(from="multipleSelectionsAllowed == true", to="multiple(this)") + @StateRefinement(from="multipleSelectionsAllowed == false", to="single(this)") + public void ChoiceCallback(String prompt, String[] choices, int defaultChoice, boolean multipleSelectionsAllowed); + + + @StateRefinement(from="multiple(this)", to="multiple(this)") + public void setSelectedIndexes(int[] selections); +} + diff --git a/examples/demo/src/main/java/com/choiceCallback/ChoiceCallbackTests.java b/examples/demo/src/main/java/com/choiceCallback/ChoiceCallbackTests.java new file mode 100644 index 0000000..5450faa --- /dev/null +++ b/examples/demo/src/main/java/com/choiceCallback/ChoiceCallbackTests.java @@ -0,0 +1,13 @@ +package com.choiceCallback; + +import javax.security.auth.callback.ChoiceCallback; + +public class ChoiceCallbackTests { + + // not supported + void example() { + boolean allowMultipleSelection = false; + ChoiceCallback cc = new ChoiceCallback(null, null, 0, allowMultipleSelection); + cc.setSelectedIndexes(null); // should be an error because allowMultipleSelection is false + } +} From 8ddeabf3a12901b78514e97f9c0a490a9cadb9d3 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 13 Jan 2026 16:00:52 +0000 Subject: [PATCH 03/11] Rename Folder --- .../main/java/com/bufferedreader/BufferedReaderRefinements.java | 2 +- .../src/main/java/com/bufferedreader/BufferedReaderTests.java | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/examples/demo/src/main/java/com/bufferedreader/BufferedReaderRefinements.java b/examples/demo/src/main/java/com/bufferedreader/BufferedReaderRefinements.java index 5af8070..4cb169d 100644 --- a/examples/demo/src/main/java/com/bufferedreader/BufferedReaderRefinements.java +++ b/examples/demo/src/main/java/com/bufferedreader/BufferedReaderRefinements.java @@ -1,4 +1,4 @@ -package com.bufferedreader; +package com.bufferedReader; import java.io.IOException; import java.io.Reader; diff --git a/examples/demo/src/main/java/com/bufferedreader/BufferedReaderTests.java b/examples/demo/src/main/java/com/bufferedreader/BufferedReaderTests.java index 6a1f86d..37ac512 100644 --- a/examples/demo/src/main/java/com/bufferedreader/BufferedReaderTests.java +++ b/examples/demo/src/main/java/com/bufferedreader/BufferedReaderTests.java @@ -1,4 +1,4 @@ -package com.bufferedreader; +package com.bufferedReader; import java.io.BufferedReader; import java.io.FileReader; From 51589788a86ef11e90721004b17cf2a1430d4fa7 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 13 Jan 2026 16:42:32 +0000 Subject: [PATCH 04/11] ZipOutputStream Refinements --- .../ZipOutputStreamRefinements.java | 49 +++++++++++++++++++ .../zipOutputStream/ZipOutputStreamTests.java | 22 +++++++++ 2 files changed, 71 insertions(+) create mode 100644 examples/demo/src/main/java/com/zipOutputStream/ZipOutputStreamRefinements.java create mode 100644 examples/demo/src/main/java/com/zipOutputStream/ZipOutputStreamTests.java diff --git a/examples/demo/src/main/java/com/zipOutputStream/ZipOutputStreamRefinements.java b/examples/demo/src/main/java/com/zipOutputStream/ZipOutputStreamRefinements.java new file mode 100644 index 0000000..8f5bb65 --- /dev/null +++ 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 new file mode 100644 index 0000000..835e786 --- /dev/null +++ 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); + } +} \ No newline at end of file From 8a1563c878bfab5a4086d221d1838fb80fe1a300 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 29 Jan 2026 15:55:26 +0000 Subject: [PATCH 05/11] Add Examples --- .../BufferedReaderRefinements.java | 39 +++++----- .../bufferedreader/BufferedReaderTests.java | 6 +- .../DragSourceContextRefinements.java | 53 +++++++++++++ .../DragSourceContextTests.java | 21 +++++ .../com/dropTarget/DropTargetRefinements.java | 58 ++++++++++++++ .../java/com/dropTarget/DropTargetTests.java | 29 +++++++ .../KerberosTicketRefinements.java | 45 +++++++++++ .../kerberosTicket/KerberosTicketTests.java | 27 +++++++ .../rmiConnector/RMIConnectorRefinements.java | 53 +++++++++++++ .../com/rmiConnector/RMIConnectorTests.java | 22 ++++++ .../serverSocket/ServerSocketRefinements.java | 76 +++++++++++++++++++ .../com/serverSocket/ServerSocketTests.java | 35 +++++++++ .../TransformerExceptionRefinements.java | 30 ++++++++ .../TransformerExceptionTests.java | 13 ++++ .../zipOutputStream/ZipOutputStreamTests.java | 4 +- 15 files changed, 487 insertions(+), 24 deletions(-) create mode 100644 examples/demo/src/main/java/com/dragSourceContext/DragSourceContextRefinements.java create mode 100644 examples/demo/src/main/java/com/dragSourceContext/DragSourceContextTests.java create mode 100644 examples/demo/src/main/java/com/dropTarget/DropTargetRefinements.java create mode 100644 examples/demo/src/main/java/com/dropTarget/DropTargetTests.java create mode 100644 examples/demo/src/main/java/com/kerberosTicket/KerberosTicketRefinements.java create mode 100644 examples/demo/src/main/java/com/kerberosTicket/KerberosTicketTests.java create mode 100644 examples/demo/src/main/java/com/rmiConnector/RMIConnectorRefinements.java create mode 100644 examples/demo/src/main/java/com/rmiConnector/RMIConnectorTests.java create mode 100644 examples/demo/src/main/java/com/serverSocket/ServerSocketRefinements.java create mode 100644 examples/demo/src/main/java/com/serverSocket/ServerSocketTests.java create mode 100644 examples/demo/src/main/java/com/transformerException/TransformerExceptionRefinements.java create mode 100644 examples/demo/src/main/java/com/transformerException/TransformerExceptionTests.java diff --git a/examples/demo/src/main/java/com/bufferedreader/BufferedReaderRefinements.java b/examples/demo/src/main/java/com/bufferedreader/BufferedReaderRefinements.java index 4cb169d..64a3084 100644 --- a/examples/demo/src/main/java/com/bufferedreader/BufferedReaderRefinements.java +++ b/examples/demo/src/main/java/com/bufferedreader/BufferedReaderRefinements.java @@ -22,37 +22,38 @@ public interface BufferedReaderRefinements { @StateRefinement(to="open(this)") public void BufferedReader(Reader in, @Refinement("Positive(_)") int sz); - @StateRefinement(from="open(this)", to="open(this)") - @StateRefinement(from="marked(this)", to="marked(this)") - public int read() throws IOException; + @StateRefinement(from="open(this)") + @StateRefinement(from="marked(this)") + public int read(); - @StateRefinement(from="open(this)", to="open(this)") - @StateRefinement(from="marked(this)", to="marked(this)") - public int read(char[] cbuf, @Refinement("NonNegative(_)") int off, @Refinement("NonNegative(_)") int len) throws IOException; // cant write "|| len <= cbuf.length - off" + @StateRefinement(from="open(this)") + @StateRefinement(from="marked(this)") + @Refinement(" _ >= -1") + public int read(char[] cbuf, @Refinement("NonNegative(_)") int off, @Refinement("NonNegative(_)") int len); - @StateRefinement(from="open(this)", to="open(this)") - @StateRefinement(from="marked(this)", to="marked(this)") + @StateRefinement(from="open(this)") + @StateRefinement(from="marked(this)") public String readLine() throws IOException; - @StateRefinement(from="open(this)", to="open(this)") - @StateRefinement(from="marked(this)", to="marked(this)") + @StateRefinement(from="open(this)") + @StateRefinement(from="marked(this)") public boolean ready() throws IOException; - @StateRefinement(from="open(this)", to="open(this)") - @StateRefinement(from="marked(this)", to="marked(this)") + @StateRefinement(from="open(this)") + @StateRefinement(from="marked(this)") public boolean markSupported(); @StateRefinement(from="open(this)", to="marked(this)") - @StateRefinement(from="marked(this)", to="marked(this)") - public void mark(@Refinement("NonNegative(_)") int readAheadLimit) throws IOException; + @StateRefinement(from="marked(this)") + public void mark(@Refinement("NonNegative(_)") int readAheadLimit); @StateRefinement(from="marked(this)", to="open(this)") - public void reset() throws IOException; + public void reset(); @StateRefinement(from="!closed(this)", to="closed(this)") - public void close() throws IOException; + public void close(); - @StateRefinement(from="open(this)", to="open(this)") - @StateRefinement(from="marked(this)", to="marked(this)") + @StateRefinement(from="open(this)") + @StateRefinement(from="marked(this)") public Stream lines(); -} +} \ No newline at end of file diff --git a/examples/demo/src/main/java/com/bufferedreader/BufferedReaderTests.java b/examples/demo/src/main/java/com/bufferedreader/BufferedReaderTests.java index 37ac512..43263d0 100644 --- a/examples/demo/src/main/java/com/bufferedreader/BufferedReaderTests.java +++ b/examples/demo/src/main/java/com/bufferedreader/BufferedReaderTests.java @@ -8,16 +8,16 @@ public class BufferedReaderTests { void readClosedFile() throws Exception { BufferedReader in = new BufferedReader(new FileReader("foo.in")); in.close(); - in.read(); + in.read(); // error } void resetUnmarkedFile() throws Exception { BufferedReader in = new BufferedReader(new FileReader("foo.in")); - in.reset(); + in.reset(); // error } void negativeLength() throws Exception { - BufferedReader in = new BufferedReader(new FileReader("foo.in"), -1); + BufferedReader in = new BufferedReader(new FileReader("foo.in"), -1); // error } void noErrors() throws Exception { diff --git a/examples/demo/src/main/java/com/dragSourceContext/DragSourceContextRefinements.java b/examples/demo/src/main/java/com/dragSourceContext/DragSourceContextRefinements.java new file mode 100644 index 0000000..929af74 --- /dev/null +++ b/examples/demo/src/main/java/com/dragSourceContext/DragSourceContextRefinements.java @@ -0,0 +1,53 @@ +package com.dragSourceContext; + +import java.awt.Cursor; +import java.awt.Image; +import java.awt.Point; +import java.awt.datatransfer.Transferable; +import java.awt.dnd.DragGestureEvent; +import java.awt.dnd.DragSourceDragEvent; +import java.awt.dnd.DragSourceDropEvent; +import java.awt.dnd.DragSourceEvent; +import java.awt.dnd.DragSourceListener; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.Refinement; +import liquidjava.specification.RefinementAlias; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@RefinementAlias("Status(int v) { 0 <= v && v <= 4 }") // DEFAULT, ENTER, OVER, CHANGED +@ExternalRefinementsFor("java.awt.dnd.DragSourceContext") +@StateSet({"noListener", "listenerSet"}) +public interface DragSourceContextRefinements { + + @StateRefinement(to="noListener(this)") + public void DragSourceContext(DragGestureEvent trigger, Cursor dragCursor, Image dragImage, Point offset, Transferable t, DragSourceListener dsl); + + @StateRefinement(from="noListener(this)", to="listenerSet(this)") + public void addDragSourceListener(DragSourceListener dsl); + + // need to use ghost variable to keep track of how many listeners are registered — this only works for a single listener at a time + @StateRefinement(from="listenerSet(this)", to="noListener(this)") + public void removeDragSourceListener(DragSourceListener dsl); + + @StateRefinement(from="listenerSet(this)") + public void dragEnter(DragSourceDragEvent dsde); + + @StateRefinement(from="listenerSet(this)") + public void dragOver(DragSourceDragEvent dsde); + + @StateRefinement(from="listenerSet(this)") + public void dragExit(DragSourceEvent dse); + + @StateRefinement(from="listenerSet(this)") + public void dropActionChanged(DragSourceDragEvent dsde); + + @StateRefinement(from="listenerSet(this)") + public void dragDropEnd(DragSourceDropEvent dsde); + + @StateRefinement(from="listenerSet(this)") + public void dragMouseMoved(DragSourceDragEvent dsde); + + public void updateCurrentCursor(int sourceAct, int targetAct, @Refinement("Status(_)") int status); +} diff --git a/examples/demo/src/main/java/com/dragSourceContext/DragSourceContextTests.java b/examples/demo/src/main/java/com/dragSourceContext/DragSourceContextTests.java new file mode 100644 index 0000000..a4caf08 --- /dev/null +++ b/examples/demo/src/main/java/com/dragSourceContext/DragSourceContextTests.java @@ -0,0 +1,21 @@ +package com.dragSourceContext; + +import java.awt.dnd.DragSourceContext; + +public class DragSourceContextTests { + + public void testRemoveUnregisteredListener() { + DragSourceContext dsc = new DragSourceContext(null, null, null, null, null, null); + dsc.removeDragSourceListener(null); // error + } + + public void testOk() throws Exception { + DragSourceContext dsc = new DragSourceContext(null, null, null, null, null, null); + dsc.addDragSourceListener(null); + dsc.removeDragSourceListener(null); + dsc.addDragSourceListener(null); + dsc.dragEnter(null); + dsc.dragExit(null); + } + +} diff --git a/examples/demo/src/main/java/com/dropTarget/DropTargetRefinements.java b/examples/demo/src/main/java/com/dropTarget/DropTargetRefinements.java new file mode 100644 index 0000000..19dda00 --- /dev/null +++ b/examples/demo/src/main/java/com/dropTarget/DropTargetRefinements.java @@ -0,0 +1,58 @@ +package com.dropTarget; + +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; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@ExternalRefinementsFor("java.awt.dnd.DropTarget") +@StateSet({"noListener", "listenerSet"}) +@StateSet({"notActive", "active"}) +public interface DropTargetRefinements { + + @StateRefinement(to="noListener(this) && notActive(this)") + public void DropTarget(Component c, int ops, DropTargetListener dtl, boolean act, FlavorMap fm); + + @StateRefinement(to="noListener(this) && notActive(this)") + public void DropTarget(Component c, int ops, DropTargetListener dtl, boolean act); + + @StateRefinement(to="noListener(this) && notActive(this)") + public void DropTarget(); + + @StateRefinement(to="noListener(this) && notActive(this)") + public void DropTarget(Component c, DropTargetListener dtl); + + @StateRefinement(to="noListener(this) && notActive(this)") + public void DropTarget(Component c, int ops, DropTargetListener dtl); + + @StateRefinement(from="isActive && notActive(this)", to="active(this)") + @StateRefinement(from="!isActive && active(this)", to="notActive(this)") + public void setActive(boolean isActive); + + @StateRefinement(from="noListener(this)", to="listenerSet(this)") + public void addDropTargetListener(DropTargetListener dtl); + + @StateRefinement(from="listenerSet(this)", to="noListener(this)") + public void removeDropTargetListener(DropTargetListener dtl); + + @StateRefinement(from="active(this)") + public void dragEnter(DropTargetDragEvent dtde); + + @StateRefinement(from="active(this)") + public void dragOver(DropTargetDragEvent dtde); + + @StateRefinement(from="active(this)") + public void dropActionChanged(DropTargetDragEvent dtde); + + @StateRefinement(from="active(this)") + public void dragExit(DropTargetEvent dtde); + + @StateRefinement(from="active(this)") + public void drop(DropTargetDropEvent dtde); +} diff --git a/examples/demo/src/main/java/com/dropTarget/DropTargetTests.java b/examples/demo/src/main/java/com/dropTarget/DropTargetTests.java new file mode 100644 index 0000000..70259ef --- /dev/null +++ b/examples/demo/src/main/java/com/dropTarget/DropTargetTests.java @@ -0,0 +1,29 @@ +package com.dropTarget; + +import java.awt.dnd.DropTarget; + +public class DropTargetTests { + + public void testDragWhenInactive() { + DropTarget dt = new DropTarget(); + dt.setActive(true); + dt.dragEnter(null); + dt.setActive(false); + dt.dragEnter(null); // error + } + + public void testRemoveUnaddedListener() { + DropTarget dt = new DropTarget(); + dt.removeDropTargetListener(null); // error + } + + public void testOk() throws Exception { + DropTarget dt = new DropTarget(); + dt.setActive(true); + dt.dragEnter(null); + dt.dragOver(null); + dt.dragExit(null); + dt.addDropTargetListener(null); + dt.removeDropTargetListener(null); + } +} diff --git a/examples/demo/src/main/java/com/kerberosTicket/KerberosTicketRefinements.java b/examples/demo/src/main/java/com/kerberosTicket/KerberosTicketRefinements.java new file mode 100644 index 0000000..ceb2b29 --- /dev/null +++ b/examples/demo/src/main/java/com/kerberosTicket/KerberosTicketRefinements.java @@ -0,0 +1,45 @@ +package com.kerberosTicket; + +import java.net.InetAddress; +import java.util.Date; + +import javax.crypto.SecretKey; +import javax.security.auth.kerberos.KerberosPrincipal; +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@ExternalRefinementsFor("javax.security.auth.kerberos.KerberosTicket") +@StateSet({"created", "destroyed"}) +public interface KerberosTicketRefinements { + + @StateRefinement(to="created(this)") + public void KerberosTicket( + byte[] asn1Encoding, + KerberosPrincipal client, + KerberosPrincipal server, + byte[] sessionKey, + int keyType, + boolean[] flags, + Date authTime, + Date startTime, + Date endTime, + Date renewTill, + InetAddress[] clientAddresses + ); + + @StateRefinement(from="created(this)") + public SecretKey getSessionKey(); + + @StateRefinement(from="created(this)") + public int getSessionKeyType(); + + @StateRefinement(from="created(this)") + public byte[] getEncoded(); + + @StateRefinement(from="created(this)") + public void refresh(); + + @StateRefinement(from="created(this)", to="destroyed(this)") + public void destroy(); +} diff --git a/examples/demo/src/main/java/com/kerberosTicket/KerberosTicketTests.java b/examples/demo/src/main/java/com/kerberosTicket/KerberosTicketTests.java new file mode 100644 index 0000000..44b14dd --- /dev/null +++ b/examples/demo/src/main/java/com/kerberosTicket/KerberosTicketTests.java @@ -0,0 +1,27 @@ +package com.kerberosTicket; + +import javax.security.auth.kerberos.KerberosTicket; + +public class KerberosTicketTests { + + public void testGetSessionKeyAfterDestroyed() throws Exception { + KerberosTicket kt = new KerberosTicket(null, null, null, null, 0, null, null, null, null, null, null); + kt.refresh(); + kt.destroy(); + kt.getSessionKey(); + } + + public void testDestroyTwice() throws Exception { + KerberosTicket kt = new KerberosTicket(null, null, null, null, 0, null, null, null, null, null, null); + kt.getEncoded(); + kt.destroy(); + kt.destroy(); + } + + public void testOk() throws Exception { + KerberosTicket kt = new KerberosTicket(null, null, null, null, 0, null, null, null, null, null, null); + kt.refresh(); + kt.getSessionKey(); + kt.destroy(); + } +} diff --git a/examples/demo/src/main/java/com/rmiConnector/RMIConnectorRefinements.java b/examples/demo/src/main/java/com/rmiConnector/RMIConnectorRefinements.java new file mode 100644 index 0000000..5aa4974 --- /dev/null +++ b/examples/demo/src/main/java/com/rmiConnector/RMIConnectorRefinements.java @@ -0,0 +1,53 @@ +package com.rmiConnector; + +import java.io.IOException; +import java.util.Map; + +import javax.management.MBeanServerConnection; +import javax.management.NotificationFilter; +import javax.management.NotificationListener; +import javax.management.remote.JMXServiceURL; +import javax.management.remote.rmi.RMIServer; +import javax.security.auth.Subject; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@ExternalRefinementsFor("javax.management.remote.rmi.RMIConnector") +@StateSet({"created", "connected", "closed"}) +public interface RMIConnectorRefinements { + + @StateRefinement(to="created(this)") + public void RMIConnector(JMXServiceURL url, Map environment); + + @StateRefinement(to="created(this)") + public void RMIConnector(RMIServer rmiServer, Map environment); + + @StateRefinement(from="created(this)", to="connected(this)") + public void connect(); + + @StateRefinement(from="created(this)", to="connected(this)") + public void connect(Map environment); + + @StateRefinement(from="connected(this)") + public String getConnectionId(); + + @StateRefinement(from="connected(this)") + public MBeanServerConnection getMBeanServerConnection(); + + @StateRefinement(from="connected(this)") + public MBeanServerConnection getMBeanServerConnection(Subject delegationSubject); + + @StateRefinement(from="connected(this)") + public void addConnectionNotificationListener(NotificationListener listener, NotificationFilter filter, Object handback); + + @StateRefinement(from="connected(this)") + public void removeConnectionNotificationListener(NotificationListener listener); + + @StateRefinement(from="connected(this)") + public void removeConnectionNotificationListener(NotificationListener listener, NotificationFilter filter, Object handback); + + @StateRefinement(from="!closed(this)", to="closed(this)") + public void close(); +} diff --git a/examples/demo/src/main/java/com/rmiConnector/RMIConnectorTests.java b/examples/demo/src/main/java/com/rmiConnector/RMIConnectorTests.java new file mode 100644 index 0000000..b1b4141 --- /dev/null +++ b/examples/demo/src/main/java/com/rmiConnector/RMIConnectorTests.java @@ -0,0 +1,22 @@ +package com.rmiConnector; + +import javax.management.remote.JMXServiceURL; +import javax.management.remote.rmi.RMIConnector; + +public class RMIConnectorTests { + + void getConnectionIdAfterClosing() throws Exception { + JMXServiceURL url = new JMXServiceURL(""); + RMIConnector rmi = new RMIConnector(url, null); + rmi.connect(); + rmi.close(); + rmi.getConnectionId(); // error + } + + void getMBeanServerConnectionWithoutConnecting() throws Exception { + JMXServiceURL url = new JMXServiceURL(""); + RMIConnector rmi = new RMIConnector(url, null); + rmi.getMBeanServerConnection(); // error + rmi.close(); + } +} diff --git a/examples/demo/src/main/java/com/serverSocket/ServerSocketRefinements.java b/examples/demo/src/main/java/com/serverSocket/ServerSocketRefinements.java new file mode 100644 index 0000000..c0150fa --- /dev/null +++ b/examples/demo/src/main/java/com/serverSocket/ServerSocketRefinements.java @@ -0,0 +1,76 @@ +package com.serverSocket; + +import java.net.InetAddress; +import java.net.Socket; +import java.net.SocketAddress; +import java.net.SocketImpl; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.Refinement; +import liquidjava.specification.RefinementAlias; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@RefinementAlias("Port(int p) { 0 <= p && p <= 65535 }") +@RefinementAlias("Positive(int n) { n >= 0 } ") +@ExternalRefinementsFor("java.net.ServerSocket") +@StateSet({"unbound", "bound", "accepted", "closed"}) +@StateSet({"hasNotBound", "hasBound"}) +public interface ServerSocketRefinements { + + @StateRefinement(to="unbound(this) && hasNotBound(this)") + public void ServerSocket(); + + @StateRefinement(to="unbound(this) && hasNotBound(this)") + public void ServerSocket(@Refinement("Port(_)") int port); + + @StateRefinement(to="unbound(this) && hasNotBound(this)") + public void ServerSocket(@Refinement("Port(_)") int port, @Refinement("Positive(_)") int backlog); + + @StateRefinement(to="unbound(this) && hasNotBound(this)") + public void ServerSocket(@Refinement("Port(_)") int port, @Refinement("Positive(_)") int backlog, InetAddress bindAddr); + + @StateRefinement(to="unbound(this) && hasNotBound(this)") + public void ServerSocket(SocketImpl impl); + + @StateRefinement(from="unbound(this)", to="bound(this) && hasBound(this)") + public void bind(SocketAddress endpoint); + + @StateRefinement(from="unbound(this)", to="bound(this) && hasBound(this)") + public void bind(SocketAddress endpoint, @Refinement("Positive(_)") int backlog); + + // If the socket was bound prior to being closed, then this method will continue to return the local address after the socket is closed. + // we need another stateset that does not lose information about whether the socket has been bound after closing or not + @StateRefinement(from="hasBound(this)") + public InetAddress getInetAddress(); + + @StateRefinement(from="hasBound(this)") + @Refinement("Port(_)") + public int getLocalPort(); + + @StateRefinement(from="hasBound(this)") + public SocketAddress getLocalSocketAddress(); + + @StateRefinement(from="bound(this)", to="accepted(this)") + public Socket accept(); + + @StateRefinement(from="bound(this)", to="accepted(this)") + public void implAccept(Socket s); + + @StateRefinement(from="!closed(this)", to="closed(this)") + public void close(); + + public void setSoTimeout(@Refinement("Positive(_)") int timeout); + + @Refinement("Positive(_)") + public int getSoTimeout(); + + @StateRefinement(from="!closed(this)") + public void setReuseAddress(boolean on); + + @StateRefinement(from="accepted(this)") + public void setReceiveBufferSize(@Refinement("Positive(_)") int size); + + @StateRefinement(from="unbound(this)") + public void setPerformancePreferences(int connectionTime, int latency, int bandwidth); +} \ No newline at end of file diff --git a/examples/demo/src/main/java/com/serverSocket/ServerSocketTests.java b/examples/demo/src/main/java/com/serverSocket/ServerSocketTests.java new file mode 100644 index 0000000..ae00445 --- /dev/null +++ b/examples/demo/src/main/java/com/serverSocket/ServerSocketTests.java @@ -0,0 +1,35 @@ +package com.serverSocket; + +import java.net.ServerSocket; +import java.net.SocketAddress; + +public class ServerSocketTests { + + private SocketAddress addr; + + public void testParametric() throws Exception { + ServerSocket s = new ServerSocket(-1, -2); // error + + } + + public void testBindTwice() throws Exception { + ServerSocket s = new ServerSocket(); + s.bind(addr); + s.bind(addr); // error + } + + public void testBindClosed() throws Exception { + ServerSocket s = new ServerSocket(); + s.close(); + s.bind(addr); // error + } + + public void testOk() throws Exception { + ServerSocket s = new ServerSocket(); + s.bind(addr); + s.accept(); + s.setReceiveBufferSize(100); + s.close(); + } +} + diff --git a/examples/demo/src/main/java/com/transformerException/TransformerExceptionRefinements.java b/examples/demo/src/main/java/com/transformerException/TransformerExceptionRefinements.java new file mode 100644 index 0000000..8b653b3 --- /dev/null +++ b/examples/demo/src/main/java/com/transformerException/TransformerExceptionRefinements.java @@ -0,0 +1,30 @@ +package com.transformerException; + +import javax.xml.transform.SourceLocator; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@ExternalRefinementsFor("javax.xml.transform.TransformerException") +@StateSet({"created", "called"}) +public interface TransformerExceptionRefinements { + + @StateRefinement(to="created(this)") + public void TransformerException(String message); + + @StateRefinement(to="created(this)") + public void TransformerException(Throwable e); + + @StateRefinement(to="created(this)") + public void TransformerException(String message, Throwable e); + + @StateRefinement(to="created(this)") + public void TransformerException(String message, SourceLocator locator); + + @StateRefinement(to="created(this)") + public void TransformerException(String message, SourceLocator locator, Throwable e); + + @StateRefinement(from="created(this)", to="called(this)") + public Throwable initCause(Throwable cause); // can only be called at most once +} diff --git a/examples/demo/src/main/java/com/transformerException/TransformerExceptionTests.java b/examples/demo/src/main/java/com/transformerException/TransformerExceptionTests.java new file mode 100644 index 0000000..6be4410 --- /dev/null +++ b/examples/demo/src/main/java/com/transformerException/TransformerExceptionTests.java @@ -0,0 +1,13 @@ +package com.transformerException; + +import javax.xml.transform.TransformerException; + +public class TransformerExceptionTests { + + public void cannotInvokeInitCauseMoreThanOnce() { + TransformerException te = new TransformerException(""); + Throwable th = new Throwable(); + te.initCause(th); + te.initCause(th); // error + } +} diff --git a/examples/demo/src/main/java/com/zipOutputStream/ZipOutputStreamTests.java b/examples/demo/src/main/java/com/zipOutputStream/ZipOutputStreamTests.java index 835e786..ca1f1ea 100644 --- a/examples/demo/src/main/java/com/zipOutputStream/ZipOutputStreamTests.java +++ b/examples/demo/src/main/java/com/zipOutputStream/ZipOutputStreamTests.java @@ -11,12 +11,12 @@ void testWritingToClosedStream() throws Exception { zos.setMethod(8); zos.setLevel(5); zos.close(); - zos.write(null, 0, 0); + zos.write(null, 0, 0); // error } void testParametricRefinements() throws Exception { FileOutputStream fos = new FileOutputStream("file"); ZipOutputStream zos = new ZipOutputStream(fos); - zos.setLevel(10); + zos.setLevel(10); // error } } \ No newline at end of file From e5bf07ec90b501e7596797edc262778427a50eef Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 29 Jan 2026 17:01:02 +0000 Subject: [PATCH 06/11] Update ChoiceCallbackRefinements --- .../java/com/choiceCallback/ChoiceCallbackRefinements.java | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/examples/demo/src/main/java/com/choiceCallback/ChoiceCallbackRefinements.java b/examples/demo/src/main/java/com/choiceCallback/ChoiceCallbackRefinements.java index b588052..f642351 100644 --- a/examples/demo/src/main/java/com/choiceCallback/ChoiceCallbackRefinements.java +++ b/examples/demo/src/main/java/com/choiceCallback/ChoiceCallbackRefinements.java @@ -8,13 +8,9 @@ @ExternalRefinementsFor("javax.security.auth.callback.ChoiceCallback") public interface ChoiceCallbackRefinements { - // not supported - @StateRefinement(from="multipleSelectionsAllowed == true", to="multiple(this)") - @StateRefinement(from="multipleSelectionsAllowed == false", to="single(this)") + @StateRefinement(to="multipleSelectionsAllowed ? multiple(this) : single(this)") public void ChoiceCallback(String prompt, String[] choices, int defaultChoice, boolean multipleSelectionsAllowed); - @StateRefinement(from="multiple(this)", to="multiple(this)") public void setSelectedIndexes(int[] selections); } - From 33acddb9154b6991c75c9df4a68a918e2d7d4145 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Fri, 30 Jan 2026 14:38:16 +0000 Subject: [PATCH 07/11] Minor Changes --- .../src/main/java/com/choiceCallback/ChoiceCallbackTests.java | 2 +- .../java/com/dragSourceContext/DragSourceContextTests.java | 1 - .../src/main/java/com/kerberosTicket/KerberosTicketTests.java | 4 ++-- .../main/java/com/rmiConnector/RMIConnectorRefinements.java | 1 - 4 files changed, 3 insertions(+), 5 deletions(-) diff --git a/examples/demo/src/main/java/com/choiceCallback/ChoiceCallbackTests.java b/examples/demo/src/main/java/com/choiceCallback/ChoiceCallbackTests.java index 5450faa..22cb482 100644 --- a/examples/demo/src/main/java/com/choiceCallback/ChoiceCallbackTests.java +++ b/examples/demo/src/main/java/com/choiceCallback/ChoiceCallbackTests.java @@ -8,6 +8,6 @@ public class ChoiceCallbackTests { void example() { boolean allowMultipleSelection = false; ChoiceCallback cc = new ChoiceCallback(null, null, 0, allowMultipleSelection); - cc.setSelectedIndexes(null); // should be an error because allowMultipleSelection is false + cc.setSelectedIndexes(null); // error } } diff --git a/examples/demo/src/main/java/com/dragSourceContext/DragSourceContextTests.java b/examples/demo/src/main/java/com/dragSourceContext/DragSourceContextTests.java index a4caf08..30b59b4 100644 --- a/examples/demo/src/main/java/com/dragSourceContext/DragSourceContextTests.java +++ b/examples/demo/src/main/java/com/dragSourceContext/DragSourceContextTests.java @@ -17,5 +17,4 @@ public void testOk() throws Exception { dsc.dragEnter(null); dsc.dragExit(null); } - } diff --git a/examples/demo/src/main/java/com/kerberosTicket/KerberosTicketTests.java b/examples/demo/src/main/java/com/kerberosTicket/KerberosTicketTests.java index 44b14dd..6b720eb 100644 --- a/examples/demo/src/main/java/com/kerberosTicket/KerberosTicketTests.java +++ b/examples/demo/src/main/java/com/kerberosTicket/KerberosTicketTests.java @@ -8,14 +8,14 @@ public void testGetSessionKeyAfterDestroyed() throws Exception { KerberosTicket kt = new KerberosTicket(null, null, null, null, 0, null, null, null, null, null, null); kt.refresh(); kt.destroy(); - kt.getSessionKey(); + kt.getSessionKey(); // error } public void testDestroyTwice() throws Exception { KerberosTicket kt = new KerberosTicket(null, null, null, null, 0, null, null, null, null, null, null); kt.getEncoded(); kt.destroy(); - kt.destroy(); + kt.destroy(); // error } public void testOk() throws Exception { diff --git a/examples/demo/src/main/java/com/rmiConnector/RMIConnectorRefinements.java b/examples/demo/src/main/java/com/rmiConnector/RMIConnectorRefinements.java index 5aa4974..8db076d 100644 --- a/examples/demo/src/main/java/com/rmiConnector/RMIConnectorRefinements.java +++ b/examples/demo/src/main/java/com/rmiConnector/RMIConnectorRefinements.java @@ -1,6 +1,5 @@ package com.rmiConnector; -import java.io.IOException; import java.util.Map; import javax.management.MBeanServerConnection; From 0d2d5470e60e5d8bb456a82a3135254176eae164 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Fri, 30 Jan 2026 15:29:27 +0000 Subject: [PATCH 08/11] Add DatagramSocket Refinements --- .../DatagramSocketRefinements.java | 87 +++++++++++++++++++ .../datagramSocket/DatagramSocketTests.java | 35 ++++++++ 2 files changed, 122 insertions(+) create mode 100644 examples/demo/src/main/java/com/datagramSocket/DatagramSocketRefinements.java create mode 100644 examples/demo/src/main/java/com/datagramSocket/DatagramSocketTests.java diff --git a/examples/demo/src/main/java/com/datagramSocket/DatagramSocketRefinements.java b/examples/demo/src/main/java/com/datagramSocket/DatagramSocketRefinements.java new file mode 100644 index 0000000..cf3ca93 --- /dev/null +++ b/examples/demo/src/main/java/com/datagramSocket/DatagramSocketRefinements.java @@ -0,0 +1,87 @@ +package com.datagramSocket; + +import java.net.DatagramPacket; +import java.net.DatagramSocket; +import java.net.InetAddress; +import java.net.SocketAddress; +import java.net.SocketOption; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.Refinement; +import liquidjava.specification.RefinementAlias; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@RefinementAlias("Port(int n) { 0 <= n && n <= 65535 }") +@RefinementAlias("NonNegative(int v) { v >= 0 }") +@RefinementAlias("Positive(int v) { v > 0 }") +@RefinementAlias("TrafficClass(int tc) { 0 <= tc && tc <= 255 }") +@ExternalRefinementsFor("java.net.DatagramSocket") +@StateSet({"unbound", "bound", "connected", "disconnected", "closed" }) +public interface DatagramSocketRefinements { + + @StateRefinement(to="bound(this)") // "Constructs a datagram socket and binds it to any available port on the local host machine" + public void DatagramSocket(); + + @StateRefinement(to="bound(this)") + public void DatagramSocket(SocketAddress bindaddr); // cant check for null value to start with unbound state + + @StateRefinement(to="bound(this)") + public void DatagramSocket(@Refinement("Port(_)") int port); + + @StateRefinement(from="unbound(this)", to="bound(this)") + public void bind(SocketAddress addr); + + @StateRefinement(from="bound(this)", to="connected(this)") + @StateRefinement(from="unbound(this)", to="connected(this)") // "If this socket is not bound then this method will first cause the socket to be bound to an address that is assigned automatically (...)" + public void connect(InetAddress address, @Refinement("Port(_)") int port); // cant check if address is null + + @StateRefinement(from="bound(this)", to="connected(this)") + @StateRefinement(from="unbound(this)", to="connected(this)") + public void connect(SocketAddress addr); // "If given an InetSocketAddress, this method behaves as if invoking connect(InetAddress,int)" + + @StateRefinement(from="connected(this)", to="disconnected(this)") + public void disconnect(); + + @StateRefinement(from="connected(this)") + public void send(DatagramPacket p); + + @StateRefinement(from="connected(this)") + public void receive(DatagramPacket p); + + @StateRefinement(from="!closed(this)", to="closed(this)") + public void close(); + + @StateRefinement(from="unbound(this)") + @StateRefinement(from="bound(this)") + @StateRefinement(from="connected(this)") + @StateRefinement(from="disconnected(this)") + public DatagramSocket setOption(SocketOption name, T value); // "IOException - if an I/O error occurs, or if the socket is closed." + + @StateRefinement(from="unbound(this)") + @StateRefinement(from="bound(this)") + @StateRefinement(from="connected(this)") + @StateRefinement(from="disconnected(this)") + public T getOption(SocketOption name); // same as above + + public void setSoTimeout(@Refinement("NonNegative(_)") int timeout); + + @Refinement("NonNegative(_)") + public int getSoTimeout(); + + public void setSendBufferSize(@Refinement("Positive(_)") int size); + + @Refinement("Positive(_)") + public int getSendBufferSize(); + + public void setReceiveBufferSize(@Refinement("Positive(_)") int size); + + @Refinement("Positive(_)") + public int getReceiveBufferSize(); + + public void setTrafficClass(@Refinement("TrafficClass(_)") int tc); + + @Refinement("TrafficClass(_)") + public int getTrafficClass(); +} + diff --git a/examples/demo/src/main/java/com/datagramSocket/DatagramSocketTests.java b/examples/demo/src/main/java/com/datagramSocket/DatagramSocketTests.java new file mode 100644 index 0000000..2e34823 --- /dev/null +++ b/examples/demo/src/main/java/com/datagramSocket/DatagramSocketTests.java @@ -0,0 +1,35 @@ +package com.datagramSocket; + +import java.net.DatagramSocket; + +public class DatagramSocketTests { + + public void testOk() throws Exception { + DatagramSocket ds = new DatagramSocket(8080); + ds.connect(null); + ds.setSoTimeout(1000); + ds.setSendBufferSize(100); + ds.setReceiveBufferSize(1000); + ds.setTrafficClass(50); + ds.send(null); + ds.send(null); + ds.receive(null); + ds.receive(null); + ds.setOption(null, null); + ds.getOption(null); + ds.disconnect(); + ds.close(); + } + + public void testSendingAfterDisconnecting() throws Exception { + DatagramSocket ds = new DatagramSocket(8080); + ds.connect(null); + ds.disconnect(); + ds.send(null); // error + } + + public void testBindingAfterAlreadyBound() throws Exception { + DatagramSocket ds = new DatagramSocket(8080); + ds.bind(null); // error + } +} From 2f1213174c5d23dcf6301296ca597160a0eeab47 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 2 Feb 2026 13:55:19 +0000 Subject: [PATCH 09/11] Add MLet Refinements --- .../main/java/com/mLet/MLetRefinements.java | 51 +++++++++++++++++++ .../src/main/java/com/mLet/MLetTests.java | 32 ++++++++++++ 2 files changed, 83 insertions(+) create mode 100644 examples/demo/src/main/java/com/mLet/MLetRefinements.java create mode 100644 examples/demo/src/main/java/com/mLet/MLetTests.java diff --git a/examples/demo/src/main/java/com/mLet/MLetRefinements.java b/examples/demo/src/main/java/com/mLet/MLetRefinements.java new file mode 100644 index 0000000..6642004 --- /dev/null +++ b/examples/demo/src/main/java/com/mLet/MLetRefinements.java @@ -0,0 +1,51 @@ +package com.mLet; + +import java.net.URL; +import java.net.URLStreamHandlerFactory; +import java.util.Set; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@ExternalRefinementsFor("javax.management.loading.MLet") +@StateSet({"unregistered", "registered"}) +public interface MLetRefinements { + + @StateRefinement(to="unregistered(this)") + public void MLet(); + + @StateRefinement(to="unregistered(this)") + public void MLet(URL[] urls); + + @StateRefinement(to="unregistered(this)") + public void MLet(URL[] urls, ClassLoader parent); + + @StateRefinement(to="unregistered(this)") + public void MLet(URL[] urls, ClassLoader parent, URLStreamHandlerFactory factory); + + @StateRefinement(to="unregistered(this)") + public void MLet(URL[] urls, boolean delegateToCLR); + + @StateRefinement(to="unregistered(this)") + public void MLet(URL[] urls, ClassLoader parent, boolean delegateToCLR); + + @StateRefinement(to="unregistered(this)") + public void MLet(URL[] urls, ClassLoader parent, URLStreamHandlerFactory factory, boolean delegateToCLR); + + // cant write "registrationDone ? registered(this) : unregistered(this)"" because it uses Boolean instead of boolean + @StateRefinement(from="unregistered(this)", to="registered(this)") + public void postRegister(Boolean registrationDone); + + @StateRefinement(from="registered(this)") + public void preDeregister(); + + @StateRefinement(from="registered(this)", to="unregistered(this)") + public void postDeregister(); + + @StateRefinement(from="registered(this)") + public Set getMBeansFromURL(URL url); + + @StateRefinement(from="registered(this)") + public Set getMBeansFromURL(String url); +} diff --git a/examples/demo/src/main/java/com/mLet/MLetTests.java b/examples/demo/src/main/java/com/mLet/MLetTests.java new file mode 100644 index 0000000..434b902 --- /dev/null +++ b/examples/demo/src/main/java/com/mLet/MLetTests.java @@ -0,0 +1,32 @@ +package com.mLet; + +import javax.management.loading.MLet; + +public class MLetTests { + + public void testOk() throws Exception { + MLet mlet = new MLet(); + mlet.addURL(""); + mlet.preRegister(null, null); + mlet.postRegister(true); + mlet.preDeregister(); + mlet.postDeregister(); + } + + public void testNotRegistering() throws Exception { + MLet mlet = new MLet(); + mlet.addURL(""); + mlet.preRegister(null, null); + mlet.getMBeansFromURL(""); // error + } + + public void testUnregisterTwice() throws Exception { + MLet mlet = new MLet(); + mlet.addURL(""); + mlet.preRegister(null, null); + mlet.postRegister(true); + mlet.preDeregister(); + mlet.postDeregister(); + mlet.postDeregister(); // error + } +} From 4f90e6d63b6c6201f3ced1bd778318be3e8c06c0 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 2 Feb 2026 14:38:16 +0000 Subject: [PATCH 10/11] Add DefaultMutableTreeNode Refinements --- .../DefaultMutableTreeNodeRefinements.java | 47 +++++++++++++++++++ .../DefaultMutableTreeNodeTests.java | 30 ++++++++++++ 2 files changed, 77 insertions(+) create mode 100644 examples/demo/src/main/java/com/defaultMutableTreeNode/DefaultMutableTreeNodeRefinements.java create mode 100644 examples/demo/src/main/java/com/defaultMutableTreeNode/DefaultMutableTreeNodeTests.java diff --git a/examples/demo/src/main/java/com/defaultMutableTreeNode/DefaultMutableTreeNodeRefinements.java b/examples/demo/src/main/java/com/defaultMutableTreeNode/DefaultMutableTreeNodeRefinements.java new file mode 100644 index 0000000..e089188 --- /dev/null +++ b/examples/demo/src/main/java/com/defaultMutableTreeNode/DefaultMutableTreeNodeRefinements.java @@ -0,0 +1,47 @@ +package com.defaultMutableTreeNode; + +import javax.swing.tree.MutableTreeNode; +import javax.swing.tree.TreeNode; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.Refinement; +import liquidjava.specification.RefinementAlias; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@RefinementAlias("Positive(int i) { i >= 0 }") +@ExternalRefinementsFor("javax.swing.tree.DefaultMutableTreeNode") +@StateSet({"childrenAllowed", "childrenNotAllowed"}) +public interface DefaultMutableTreeNodeRefinements { + + @StateRefinement(to="childrenAllowed(this)") + public void DefaultMutableTreeNode(); + + @StateRefinement(to="childrenAllowed(this)") + public void DefaultMutableTreeNode(Object userObject); + + @StateRefinement(to="allowsChildren ? childrenAllowed(this) : childrenNotAllowed(this)") + public void DefaultMutableTreeNode(Object userObject, boolean allowsChildren); + + @StateRefinement(from="childrenAllowed(this)") + public void insert(MutableTreeNode newChild, @Refinement("Positive(_)") int childIndex); + + @StateRefinement(from="childrenAllowed(this)") + public void add(MutableTreeNode newChild); + + @StateRefinement(to="allows ? childrenAllowed(this) : childrenNotAllowed(this)") + public void setAllowsChildren(boolean allows); + + @Refinement("childrenAllowed(this) ? true : false") + public boolean getAllowsChildren(); + + public void remove(@Refinement("Positive(_)") int childIndex); + + public TreeNode getChildAt(@Refinement("Positive(_)") int index); + + @Refinement("Positive(_)") + public int getChildCount(); + + @Refinement("Positive(_) || _ == -1") + public int getIndex(TreeNode aChild); +} diff --git a/examples/demo/src/main/java/com/defaultMutableTreeNode/DefaultMutableTreeNodeTests.java b/examples/demo/src/main/java/com/defaultMutableTreeNode/DefaultMutableTreeNodeTests.java new file mode 100644 index 0000000..b694a4b --- /dev/null +++ b/examples/demo/src/main/java/com/defaultMutableTreeNode/DefaultMutableTreeNodeTests.java @@ -0,0 +1,30 @@ +package com.defaultMutableTreeNode; + +import javax.swing.tree.DefaultMutableTreeNode; + +public class DefaultMutableTreeNodeTests { + + public void testOk() { + DefaultMutableTreeNode node = new DefaultMutableTreeNode(); + node.insert(null, 0); + node.getIndex(null); + node.remove(0); + } + + public void testAddUnwantedChildConstructor() { + DefaultMutableTreeNode node = new DefaultMutableTreeNode(null, false); + node.insert(null, 0); // error + } + + public void testAddUnwantedChildSetter() { + DefaultMutableTreeNode node = new DefaultMutableTreeNode(null, true); + node.insert(null, 0); + node.setAllowsChildren(false); + node.add(null); // error + } + + public void testAddChildInvalidIndex() { + DefaultMutableTreeNode node = new DefaultMutableTreeNode(); + node.insert(null, -1); // error + } +} From 622709fbb97980cc882013aa7c27c2714f511586 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Fri, 13 Feb 2026 17:16:18 +0000 Subject: [PATCH 11/11] Update DatagramSocketTests --- .../datagramSocket/DatagramSocketTests.java | 20 +++++++++++++++---- 1 file changed, 16 insertions(+), 4 deletions(-) diff --git a/examples/demo/src/main/java/com/datagramSocket/DatagramSocketTests.java b/examples/demo/src/main/java/com/datagramSocket/DatagramSocketTests.java index 2e34823..93aecb2 100644 --- a/examples/demo/src/main/java/com/datagramSocket/DatagramSocketTests.java +++ b/examples/demo/src/main/java/com/datagramSocket/DatagramSocketTests.java @@ -21,15 +21,27 @@ public void testOk() throws Exception { ds.close(); } - public void testSendingAfterDisconnecting() throws Exception { + public void testBindTwice() throws Exception { DatagramSocket ds = new DatagramSocket(8080); - ds.connect(null); - ds.disconnect(); - ds.send(null); // error + ds.bind(null); // error } public void testBindingAfterAlreadyBound() throws Exception { DatagramSocket ds = new DatagramSocket(8080); ds.bind(null); // error } + + public void testConnectingAfterClosing() throws Exception { + DatagramSocket ds = new DatagramSocket(8080); + ds.connect(null); + ds.close(); + ds.connect(null); // error + } + + public void testBound() throws Exception { + DatagramSocket ds = new DatagramSocket(8080); + if (!ds.isBound()) { + ds.bind(null); // this should not be an error + } + } }