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..64a3084 --- /dev/null +++ b/examples/demo/src/main/java/com/bufferedreader/BufferedReaderRefinements.java @@ -0,0 +1,59 @@ +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)") + @StateRefinement(from="marked(this)") + public int read(); + + @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)") + @StateRefinement(from="marked(this)") + public String readLine() throws IOException; + + @StateRefinement(from="open(this)") + @StateRefinement(from="marked(this)") + public boolean ready() throws IOException; + + @StateRefinement(from="open(this)") + @StateRefinement(from="marked(this)") + public boolean markSupported(); + + @StateRefinement(from="open(this)", to="marked(this)") + @StateRefinement(from="marked(this)") + public void mark(@Refinement("NonNegative(_)") int readAheadLimit); + + @StateRefinement(from="marked(this)", to="open(this)") + public void reset(); + + @StateRefinement(from="!closed(this)", to="closed(this)") + public void close(); + + @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 new file mode 100644 index 0000000..43263d0 --- /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(); // error + } + + void resetUnmarkedFile() throws Exception { + BufferedReader in = new BufferedReader(new FileReader("foo.in")); + in.reset(); // error + } + + void negativeLength() throws Exception { + BufferedReader in = new BufferedReader(new FileReader("foo.in"), -1); // error + } + + 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/choiceCallback/ChoiceCallbackRefinements.java b/examples/demo/src/main/java/com/choiceCallback/ChoiceCallbackRefinements.java new file mode 100644 index 0000000..f642351 --- /dev/null +++ b/examples/demo/src/main/java/com/choiceCallback/ChoiceCallbackRefinements.java @@ -0,0 +1,16 @@ +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 { + + @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); +} 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..22cb482 --- /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); // error + } +} 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..93aecb2 --- /dev/null +++ b/examples/demo/src/main/java/com/datagramSocket/DatagramSocketTests.java @@ -0,0 +1,47 @@ +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 testBindTwice() throws Exception { + DatagramSocket ds = new DatagramSocket(8080); + 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 + } + } +} 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 + } +} 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..30b59b4 --- /dev/null +++ b/examples/demo/src/main/java/com/dragSourceContext/DragSourceContextTests.java @@ -0,0 +1,20 @@ +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/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/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..6b720eb --- /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(); // 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(); // error + } + + 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/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 + } +} 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..8db076d --- /dev/null +++ b/examples/demo/src/main/java/com/rmiConnector/RMIConnectorRefinements.java @@ -0,0 +1,52 @@ +package com.rmiConnector; + +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/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..ca1f1ea --- /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); // error + } + + void testParametricRefinements() throws Exception { + FileOutputStream fos = new FileOutputStream("file"); + ZipOutputStream zos = new ZipOutputStream(fos); + zos.setLevel(10); // error + } +} \ No newline at end of file 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 ); - } -}