Skip to content

Commit c41f516

Browse files
pcanelaspcanelas
committed
feat: add Java refinements for DragSourceContext, DropTarget, and ServerSocket APIs
1 parent 684d3a2 commit c41f516

File tree

8 files changed

+344
-0
lines changed

8 files changed

+344
-0
lines changed

‎examples/demo/src/main/java/com/barista/dragsourcecontext/DragSourceContextRefinements.java‎

Lines changed: 54 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,54 @@
1+
package com.barista.dragsourcecontext;
2+
3+
import liquidjava.specification.StateSet;
4+
import liquidjava.specification.StateRefinement;
5+
import liquidjava.specification.ExternalRefinementsFor;
6+
7+
import java.awt.Cursor;
8+
import java.awt.Image;
9+
import java.awt.Point;
10+
import java.awt.datatransfer.Transferable;
11+
import java.awt.dnd.DragSourceListener;
12+
import java.awt.dnd.DragGestureEvent;
13+
import java.awt.dnd.DragSourceDragEvent;
14+
import java.awt.dnd.DragSourceDropEvent;
15+
import java.awt.dnd.DragSourceEvent;
16+
17+
@StateSet({"withListener", "noListener"})
18+
@ExternalRefinementsFor("java.awt.dnd.DragSourceContext")
19+
public interface DragSourceContextRefinements {
20+
21+
// @StateRefinement(to="dsl == null ? withListener(this) : noListener(this)")
22+
@StateRefinement(to="withListener(this)")
23+
public void DragSourceContext(DragGestureEvent trigger,
24+
Cursor dragCursor,
25+
Image dragImage,
26+
Point offset,
27+
Transferable t,
28+
DragSourceListener dsl);
29+
30+
@StateRefinement(from="noListener(this)", to="withListener(this)")
31+
public void addDragSourceListener(DragSourceListener dsl);
32+
33+
@StateRefinement(from="withListener(this)", to="noListener(this)")
34+
public void removeDragSourceListener(DragSourceListener dsl);
35+
36+
// Assumption: we always need listeners to enter drag operations
37+
@StateRefinement(from="withListener(this)", to="withListener(this)")
38+
public void dragEnter(DragSourceDragEvent dsde);
39+
40+
@StateRefinement(from="withListener(this)", to="withListener(this)")
41+
public void dragOver(DragSourceDragEvent dsde);
42+
43+
@StateRefinement(from="withListener(this)", to="withListener(this)")
44+
public void dragExit(DragSourceEvent dse);
45+
46+
@StateRefinement(from="withListener(this)", to="withListener(this)")
47+
public void dropActionChanged(DragSourceDragEvent dsde);
48+
49+
@StateRefinement(from="withListener(this)", to="withListener(this)")
50+
public void dragDropEnd(DragSourceDropEvent dsde);
51+
52+
@StateRefinement(from="withListener(this)", to="withListener(this)")
53+
public void dragMouseMoved(DragSourceDragEvent dsde);
54+
}

‎examples/demo/src/main/java/com/barista/dragsourcecontext/DragSourceContextTests.java‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
package com.barista.dragsourcecontext;
2+
3+
import java.awt.dnd.DragSourceContext;
4+
import java.util.TooManyListenersException;
5+
6+
public class DragSourceContextTests {
7+
public void test1() throws TooManyListenersException {
8+
DragSourceContext dnd = new DragSourceContext(null, null, null, null, null, null);
9+
dnd.removeDragSourceListener(null);
10+
dnd.dragOver(null);
11+
dnd.addDragSourceListener(dnd);
12+
}
13+
}

‎examples/demo/src/main/java/com/barista/droptarget/DropTargetRefinements.java‎

Lines changed: 74 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,74 @@
1+
package com.barista.droptarget;
2+
3+
import liquidjava.specification.StateSet;
4+
import liquidjava.specification.StateRefinement;
5+
6+
import java.awt.Component;
7+
import java.awt.datatransfer.FlavorMap;
8+
import java.awt.dnd.DropTargetDragEvent;
9+
import java.awt.dnd.DropTargetDropEvent;
10+
import java.awt.dnd.DropTargetEvent;
11+
import java.awt.dnd.DropTargetListener;
12+
13+
import liquidjava.specification.ExternalRefinementsFor;
14+
15+
@StateSet({"noListenerOrComponent", "withListener", "withComponent", "withListenerAndComponent", "active"})
16+
@ExternalRefinementsFor("java.awt.dnd.DropTarget")
17+
public interface DropTargetRefinements {
18+
19+
@StateRefinement(to="act ? active(this) : withListenerAndComponent(this)")
20+
public void DropTarget(Component c,
21+
int ops,
22+
DropTargetListener dtl,
23+
boolean act,
24+
FlavorMap fm
25+
);
26+
27+
@StateRefinement(to="act ? active(this) : withListener(this)")
28+
public void DropTarget(Component c,
29+
int ops,
30+
DropTargetListener dtl,
31+
boolean act
32+
);
33+
34+
@StateRefinement(to="withListenerAndComponent(this)")
35+
public void DropTarget(Component c, int ops, DropTargetListener dtl);
36+
37+
@StateRefinement(to="withListenerAndComponent(this)")
38+
public void DropTarget(Component c, DropTargetListener dtl);
39+
40+
@StateRefinement(to="noListenerOrComponent(this)")
41+
public void DropTarget();
42+
43+
@StateRefinement(from="withListener(this)", to="withListenerAndComponent(this)")
44+
@StateRefinement(from="noListenerOrComponent(this)", to="withComponent(this)")
45+
public void setComponent(Component c);
46+
47+
@StateRefinement(from="noListenerOrComponent(this)", to="withListener(this)")
48+
@StateRefinement(from="withComponent(this)", to="withListener(this)")
49+
public void addDropTargetListener(DropTargetListener dtl);
50+
51+
@StateRefinement(from="withListenerAndComponent(this)", to="withComponent(this)")
52+
@StateRefinement(from="active(this)", to="withComponent(this)")
53+
@StateRefinement(from="withListener(this)", to="noListenerOrComponent(this)")
54+
public void removeDropTargetListener(DropTargetListener dtl);
55+
56+
@StateRefinement(from="withListenerAndComponent(this)", to="isActive ? active(this) : withListenerAndComponent(this)")
57+
@StateRefinement(from="active(this)", to="isActive ? active(this) : withListenerAndComponent(this)")
58+
public void setActive(boolean isActive);
59+
60+
@StateRefinement(from="active(this)", to="active(this)")
61+
public void dragEnter(DropTargetDragEvent dtde);
62+
63+
@StateRefinement(from="active(this)", to="active(this)")
64+
public void dragOver(DropTargetDragEvent dtde);
65+
66+
@StateRefinement(from="active(this)", to="active(this)")
67+
public void dropActionChanged(DropTargetDragEvent dtde);
68+
69+
@StateRefinement(from="active(this)", to="active(this)")
70+
public void dragExit(DropTargetEvent dte);
71+
72+
@StateRefinement(from="active(this)", to="active(this)")
73+
public void drop(DropTargetDropEvent dtde);
74+
}

‎examples/demo/src/main/java/com/barista/droptarget/DropTargetTest.java‎

Lines changed: 55 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,55 @@
1+
package com.barista.droptarget;
2+
3+
import java.awt.dnd.DropTarget;
4+
import java.util.TooManyListenersException;
5+
6+
public class DropTargetTest {
7+
public void test1() {
8+
DropTarget dt = new DropTarget();
9+
dt.setActive(true);
10+
}
11+
12+
public void test2() {
13+
DropTarget dt = new DropTarget(null, null);
14+
dt.dragEnter(null);
15+
}
16+
17+
public void test3() {
18+
DropTarget dt = new DropTarget(null, 1, null, false);
19+
dt.dragEnter(null);
20+
}
21+
22+
public void test4() {
23+
DropTarget dt = new DropTarget(null, 1, null, true);
24+
dt.dragEnter(null);
25+
}
26+
27+
public void test5() throws TooManyListenersException {
28+
DropTarget dt = new DropTarget();
29+
dt.addDropTargetListener(null);
30+
dt.dragEnter(null);
31+
}
32+
33+
public void test6() throws TooManyListenersException {
34+
DropTarget dt = new DropTarget();
35+
dt.addDropTargetListener(null);
36+
dt.setActive(false);
37+
dt.dragEnter(null);
38+
}
39+
40+
public void test7() throws TooManyListenersException {
41+
DropTarget dt = new DropTarget();
42+
dt.addDropTargetListener(null);
43+
dt.setActive(true);
44+
}
45+
46+
public void test8() throws TooManyListenersException {
47+
DropTarget dt = new DropTarget();
48+
dt.addDropTargetListener(null);
49+
dt.setComponent(null);
50+
dt.setActive(true);
51+
dt.dragEnter(null);
52+
dt.setActive(false);
53+
dt.dragEnter(null);
54+
}
55+
}

‎examples/demo/src/main/java/com/barista/serversocket/ServerSocketRefinements.java‎

Lines changed: 76 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,76 @@
1+
package com.barista.serversocket;
2+
3+
import liquidjava.specification.Refinement;
4+
import liquidjava.specification.RefinementAlias;
5+
import liquidjava.specification.StateSet;
6+
import liquidjava.specification.StateRefinement;
7+
8+
import java.net.InetAddress;
9+
import java.net.ServerSocket;
10+
import java.net.SocketAddress;
11+
import java.net.SocketOption;
12+
13+
import liquidjava.specification.ExternalRefinementsFor;
14+
15+
@StateSet({"unconnected", "binded", "connected", "closed"})
16+
@RefinementAlias("Positive(int x) {x >= 0}")
17+
@ExternalRefinementsFor("java.net.ServerSocket")
18+
public interface ServerSocketRefinements {
19+
20+
// Constructors
21+
@StateRefinement(to="unconnected(this)")
22+
public void ServerSocket();
23+
24+
@StateRefinement(to="binded(this)")
25+
public void ServerSocket(@Refinement("Positive(_)") int port);
26+
27+
@StateRefinement(to="binded(this)")
28+
public void ServerSocket(
29+
@Refinement("Positive(_)") int port,
30+
@Refinement("Positive(_)") int backlog);
31+
32+
@StateRefinement(to="connected(this)")
33+
public void ServerSocket(
34+
@Refinement("Positive(_)") int port,
35+
@Refinement("Positive(_)") int backlog,
36+
InetAddress bindAddr);
37+
38+
// Methods
39+
@StateRefinement(from="unconnected(this)", to="binded(this)")
40+
public void bind(SocketAddress bindpoint);
41+
42+
@StateRefinement(from="unconnected(this)", to="binded(this)")
43+
public void bind(SocketAddress bindpoint, int backlog);
44+
45+
@StateRefinement(from="unconnected(this) || connected(this) || binded(this)", to="closed(this)")
46+
public void close();
47+
48+
@StateRefinement(from="unconnected(this)", to="unconnected(this)")
49+
@StateRefinement(from="binded(this)", to="binded(this)")
50+
@StateRefinement(from="connected(this)", to="connected(this)")
51+
public void setSoTimeout(@Refinement("Positive(_)") int timeout);
52+
53+
@StateRefinement(from="unconnected(this)", to="unconnected(this)")
54+
@StateRefinement(from="binded(this)", to="binded(this)")
55+
@StateRefinement(from="connected(this)", to="connected(this)")
56+
public void setReuseAddress(boolean on);
57+
58+
@StateRefinement(from="unconnected(this)", to="unconnected(this)")
59+
@StateRefinement(from="binded(this)", to="binded(this)")
60+
public void setPerformancePreferences(int connectionTime, int latency, int bandwith);
61+
62+
@StateRefinement(from="unconnected(this)", to="unconnected(this)")
63+
@StateRefinement(from="binded(this)", to="binded(this)")
64+
@StateRefinement(from="connected(this)", to="connected(this)")
65+
public <T> ServerSocket setOption(SocketOption<T> name, T value);
66+
67+
@StateRefinement(from="unconnected(this)", to="unconnected(this)")
68+
@StateRefinement(from="binded(this)", to="binded(this)")
69+
@StateRefinement(from="connected(this)", to="connected(this)")
70+
public <T> T getOption(SocketOption<T> name);
71+
72+
@StateRefinement(from="binded(this)", to="binded(this)")
73+
@StateRefinement(from="unconnected(this)", to="unconnected(this)")
74+
@StateRefinement(from="!(size >= 64000) && connected(this)", to="connected(this)")
75+
public void setReceiveBufferSize(int size);
76+
}

‎examples/demo/src/main/java/com/barista/serversocket/ServerSocketTests.java‎

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
package com.barista.serversocket;
2+
3+
import java.io.IOException;
4+
import java.net.ServerSocket;
5+
6+
public class ServerSocketTests {
7+
8+
9+
public static void test1() throws IOException {
10+
ServerSocket s = new ServerSocket();
11+
s.close();
12+
s.bind(null);
13+
}
14+
15+
public static void test2() throws IOException {
16+
ServerSocket s = new ServerSocket(8080);
17+
s.bind(null);
18+
}
19+
20+
public static void test3() throws IOException {
21+
ServerSocket s = new ServerSocket();
22+
s.bind(null);
23+
s.bind(null);
24+
}
25+
26+
27+
}

‎examples/demo/src/main/java/com/barista/throwable/ThrowableRefinements.java‎

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
package com.barista.throwable;
2+
3+
import liquidjava.specification.StateSet;
4+
import liquidjava.specification.StateRefinement;
5+
import liquidjava.specification.ExternalRefinementsFor;
6+
7+
@StateSet({"withThrowable", "noThrowable"})
8+
@ExternalRefinementsFor("java.lang.Throwable")
9+
public interface ThrowableRefinements {
10+
11+
@StateRefinement(to="noThrowable(this)")
12+
public void Throwable();
13+
14+
@StateRefinement(to="noThrowable(this)")
15+
public void Throwable(String message);
16+
17+
@StateRefinement(to="withThrowable(this)")
18+
public void Throwable(String message, Throwable cause);
19+
20+
@StateRefinement(to="withThrowable(this)")
21+
public void Throwable(Throwable cause);
22+
23+
@StateRefinement(to="withThrowable(this)")
24+
public void Throwable(String message, Throwable cause, boolean enableSuppression, boolean writableStackTrace);
25+
26+
@StateRefinement(from="noThrowable(this)", to="withThrowable(this)")
27+
public Throwable initCause(Throwable cause);
28+
}

‎examples/demo/src/main/java/com/barista/throwable/ThrowableTest.java‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
package com.barista.throwable;
2+
3+
import java.lang.Throwable;
4+
5+
public class ThrowableTest {
6+
public void test1() {
7+
Throwable x = new Throwable();
8+
x.initCause(x);
9+
x.initCause(x);
10+
}
11+
12+
public void test2() {
13+
Throwable x = new Throwable();
14+
Throwable y = new Throwable(x);
15+
x.initCause(y);
16+
}
17+
}

0 commit comments

Comments
 (0)