diff --git a/examples/demo/src/main/java/com/abstractundo/AbstractUndoRefinements.java b/examples/demo/src/main/java/com/abstractundo/AbstractUndoRefinements.java new file mode 100644 index 0000000..514e6bd --- /dev/null +++ b/examples/demo/src/main/java/com/abstractundo/AbstractUndoRefinements.java @@ -0,0 +1,39 @@ +package com.abstractundo; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + + + +@StateSet({"aliveDone", "aliveNotDone", "notAlive"}) +@ExternalRefinementsFor("javax.swing.undo.AbstractUndoableEdit") +public interface AbstractUndoRefinements { + + @StateRefinement(to="aliveDone(this)") + void AbstractUndoableEdit(); + + @StateRefinement(from="aliveNotDone(this)", to="aliveDone(this)") + void redo(); + + @StateRefinement(from="aliveDone(this)", to="aliveNotDone(this)") + void undo(); + + @StateRefinement(from="!notAlive(this)", to="notAlive(this)") + void die(); + + + // anything + // boolean canRedo(); + // boolean canUndo(); + + // boolean addEdit(UndoableEdit anEdit); + // String getPresentationName(); + // String getRedoPresentationName(); + // String getUndoPresentationName(); + // boolean isSignificant(); + // boolean replaceEdit(UndoableEdit anEdit); + // String toString(); + + +} diff --git a/examples/demo/src/main/java/com/abstractundo/TestAbstractUndo.java b/examples/demo/src/main/java/com/abstractundo/TestAbstractUndo.java new file mode 100644 index 0000000..511fcff --- /dev/null +++ b/examples/demo/src/main/java/com/abstractundo/TestAbstractUndo.java @@ -0,0 +1,28 @@ +package com.abstractundo; + +import javax.swing.undo.AbstractUndoableEdit; + +public class TestAbstractUndo { + + void test1(){ + AbstractUndoableEdit a = new AbstractUndoableEdit(); + a.redo(); + } + + void test2(){ + AbstractUndoableEdit a = new AbstractUndoableEdit(); + a.undo(); + a.redo(); + a.undo(); + a.undo(); + } + + void test3(){ + AbstractUndoableEdit a = new AbstractUndoableEdit(); + a.undo(); + a.redo(); + a.undo(); + a.die(); + a.redo(); + } +} 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..56598f2 --- /dev/null +++ b/examples/demo/src/main/java/com/mlet/MLetRefinements.java @@ -0,0 +1,62 @@ +package com.mlet; + +import java.io.ObjectInput; +import java.io.ObjectOutput; +import java.net.URL; +import java.net.URLStreamHandlerFactory; +import java.util.Set; + +import javax.management.MBeanServer; +import javax.management.ObjectName; +import javax.management.loading.ClassLoaderRepository; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@ExternalRefinementsFor("javax.management.loading.MLet") +@StateSet({"start", "preRegistered", "registered", "preDeregistered"}) +public interface MLetRefinements { + + @StateRefinement(to="start(this)") + void MLet(); + @StateRefinement(to="start(this)") + void MLet(URL[] urls); + @StateRefinement(to="start(this)") + void MLet(URL[] urls, boolean delegateToCLR); + @StateRefinement(to="start(this)") + void MLet(URL[] urls, ClassLoader parent); + @StateRefinement(to="start(this)") + void MLet(URL[] urls, ClassLoader parent, boolean delegateToCLR); + @StateRefinement(to="start(this)") + void MLet(URL[] urls, ClassLoader parent, URLStreamHandlerFactory factory); + @StateRefinement(to="start(this)") + void MLet(URL[] urls, ClassLoader parent, URLStreamHandlerFactory factory, boolean delegateToCLR); + + + @StateRefinement(from="start(this)", to="preRegistered(this)") + ObjectName preRegister(MBeanServer server, ObjectName name); + @StateRefinement(from="preRegistered(this)", to="registered(this)") + void postRegister(Boolean registrationDone); + @StateRefinement(from="registered(this)", to="preDeregistered(this)") + void preDeregister(); + @StateRefinement(from="preDeregistered(this)", to="start(this)") + void postDeregister(); + + @StateRefinement(from="registered(this)") + Set getMBeansFromURL(String url); + @StateRefinement(from="registered(this)") + Set getMBeansFromURL(URL url); + + + // void addURL(String url); + // void addURL(URL url); + // String getLibraryDirectory(); + + // URL[] getURLs(); + // Class loadClass(String name, ClassLoaderRepository clr); + // void readExternal(ObjectInput in); + // void setLibraryDirectory(String libdir); + // void writeExternal(ObjectOutput out); + +} diff --git a/examples/demo/src/main/java/com/mlet/TestMLet.java b/examples/demo/src/main/java/com/mlet/TestMLet.java new file mode 100644 index 0000000..5459d54 --- /dev/null +++ b/examples/demo/src/main/java/com/mlet/TestMLet.java @@ -0,0 +1,53 @@ +package com.mlet; + +import javax.management.loading.MLet; + +public class TestMLet { + + void test1() throws Exception{ + MLet m = new MLet(); + m.preDeregister(); + } + + void test2() throws Exception{ + MLet m = new MLet(); + m.addURL("null"); + m.preRegister(null, null); + m.preDeregister(); + m.postDeregister(); + } + + void test3() throws Exception{ + MLet m = new MLet(); + m.addURL("null"); + m.preRegister(null, null); + m.postRegister(null); + m.preDeregister(); + m.setLibraryDirectory(null); + m.getMBeansFromURL("null"); + } + + void test4() throws Exception{ + MLet m = new MLet(); + m.addURL("null"); + m.preRegister(null, null); + m.postRegister(null); + m.preDeregister(); + m.setLibraryDirectory(null); + m.preDeregister(); + } + + + void testGood() throws Exception{ + MLet m = new MLet(); + m.addURL("null"); + m.preRegister(null, null); + m.postRegister(null); + + m.getMBeansFromURL("null"); + + m.preDeregister(); + m.postDeregister(); + } + +} diff --git a/examples/demo/src/main/java/com/pipedwriter/PipedWriterRefinements.java b/examples/demo/src/main/java/com/pipedwriter/PipedWriterRefinements.java new file mode 100644 index 0000000..33ddbf1 --- /dev/null +++ b/examples/demo/src/main/java/com/pipedwriter/PipedWriterRefinements.java @@ -0,0 +1,36 @@ +package com.pipedwriter; + +import java.io.PipedReader; +import java.io.PipedWriter; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.Refinement; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@ExternalRefinementsFor("java.io.PipedWriter") +@StateSet({"started", "connected", "closed"}) +public interface PipedWriterRefinements { + + @StateRefinement(to="started(this)") + void PipedWriter(); + + @StateRefinement(to="started(this)") + void PipedWriter(PipedReader snk); + + @StateRefinement(from="!closed(this)", to="closed(this)") + void close(); + + @StateRefinement(from="started(this)", to="connected(this)") + void connect(PipedReader snk); + + @StateRefinement(from="connected(this)") + void flush(); + + @StateRefinement(from="connected(this)") + void write(char[] cbuf, @Refinement("_ > 0") int off, @Refinement("_ > 0") int len); + + @StateRefinement(from="connected(this)") + void write(int c); + +} diff --git a/examples/demo/src/main/java/com/pipedwriter/Test.java b/examples/demo/src/main/java/com/pipedwriter/Test.java new file mode 100644 index 0000000..da0c1b1 --- /dev/null +++ b/examples/demo/src/main/java/com/pipedwriter/Test.java @@ -0,0 +1,33 @@ +package com.pipedwriter; + +import java.io.IOException; +import java.io.PipedReader; +import java.io.PipedWriter; + +public class Test { + + void test1() throws IOException{ + PipedWriter pw = new PipedWriter(); + pw.write(0); + } + + void test2()throws IOException{ + PipedWriter pw = new PipedWriter(); + pw.connect(new PipedReader()); + pw.write("null"); + pw.flush(); + pw.close(); + pw.write(0); + } + + + void test3()throws IOException{ + PipedWriter pw = new PipedWriter(); + pw.connect(new PipedReader()); + pw.write("null"); + pw.flush(); + pw.close(); + pw.write(0); + } + +} diff --git a/examples/demo/src/main/java/com/requiredmodelbean/RequiredModelMBeanRefinements.java b/examples/demo/src/main/java/com/requiredmodelbean/RequiredModelMBeanRefinements.java new file mode 100644 index 0000000..96474a0 --- /dev/null +++ b/examples/demo/src/main/java/com/requiredmodelbean/RequiredModelMBeanRefinements.java @@ -0,0 +1,77 @@ +package com.requiredmodelbean; + +import javax.management.MBeanServer; +import javax.management.ObjectName; +import javax.management.modelmbean.ModelMBeanInfo; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@ExternalRefinementsFor("javax.management.modelmbean.RequiredModelMBean") +@StateSet({"unregistered", "preRegistered", "registered", "preUnregistered"}) +interface RequiredModelMBeanRefinements{ + + @StateRefinement(to="unregistered(this)") + void RequiredModelMBean(); + + @StateRefinement(to="unregistered(this)") + void RequiredModelMBean(ModelMBeanInfo mbi); + + @StateRefinement(from="unregistered(this)", to="preRegistered(this)") + ObjectName preRegister(MBeanServer server, ObjectName name); + + @StateRefinement(from="preRegistered(this)", to="registered(this)") + void postRegister(Boolean registrationDone); + + @StateRefinement(from="registered(this)", to="preUnregistered(this)") + void preDeregister(); + + @StateRefinement(from="preUnregistered(this)", to="unregistered(this)") + void postDeregister(); + + @StateRefinement(from="unregistered(this)") + void setModelMBeanInfo(ModelMBeanInfo mbi); + + @StateRefinement(from="unregistered(this)") + void load(); + + // void addAttributeChangeNotificationListener(NotificationListener inlistener, String inAttributeName, Object inhandback); + + // void addNotificationListener(NotificationListener listener, NotificationFilter filter, Object handback); + + // Object getAttribute(String attrName); + + // AttributeList getAttributes(String[] attrNames); + + // MBeanInfo getMBeanInfo(); + + // MBeanNotificationInfo[] getNotificationInfo(); + + // Object invoke(String opName, Object[] opArgs, String[] sig); + + // void removeAttributeChangeNotificationListener(NotificationListener inlistener, String inAttributeName); + + // void removeNotificationListener(NotificationListener listener); + + // void removeNotificationListener(NotificationListener listener, NotificationFilter filter, Object handback); + + // void sendAttributeChangeNotification(AttributeChangeNotification ntfyObj); + + // void sendAttributeChangeNotification(Attribute inOldVal, Attribute inNewVal); + + // void sendNotification(String ntfyText); + + // void sendNotification(Notification ntfyObj); + + // void setAttribute(Attribute attribute); + + // AttributeList setAttributes(AttributeList attributes); + + // void setManagedResource(Object mr, String mr_type); + + // void store(); + + + +} \ No newline at end of file diff --git a/examples/demo/src/main/java/com/requiredmodelbean/TestRequiredModel.java b/examples/demo/src/main/java/com/requiredmodelbean/TestRequiredModel.java new file mode 100644 index 0000000..f6cb544 --- /dev/null +++ b/examples/demo/src/main/java/com/requiredmodelbean/TestRequiredModel.java @@ -0,0 +1,34 @@ +package com.requiredmodelbean; + +import javax.management.modelmbean.ModelMBeanInfo; +import javax.management.modelmbean.RequiredModelMBean; + +public class TestRequiredModel { + + void test1() throws Exception { + RequiredModelMBean r = new RequiredModelMBean(); + r.setModelMBeanInfo(null); + r.postRegister(Boolean.TRUE); + r.setModelMBeanInfo(null); //error + } + + void test2() throws Exception { + RequiredModelMBean r = new RequiredModelMBean(); + r.setModelMBeanInfo(null); + r.setModelMBeanInfo(null); + r.setManagedResource(r, null); + r.postRegister(null); + r.load(); //error + } + + void test3() throws Exception { + RequiredModelMBean r = new RequiredModelMBean(); + r.setModelMBeanInfo(null); + r.load(); + r.setManagedResource(r, null); + r.postRegister(null); + r.store(); + r.postDeregister(); + r.load(); + } +} diff --git a/examples/demo/src/main/java/com/undomanager/TestUndoManager.java b/examples/demo/src/main/java/com/undomanager/TestUndoManager.java new file mode 100644 index 0000000..d837986 --- /dev/null +++ b/examples/demo/src/main/java/com/undomanager/TestUndoManager.java @@ -0,0 +1,41 @@ + +package com.undomanager; + +import javax.swing.undo.UndoManager; + +public class TestUndoManager { + + void test1(){ + UndoManager u = new UndoManager(); + u.addEdit(null); + u.redo(); + u.setLimit(10); + u.redo(); + u.end(); + u.setLimit(10); //error + } + + void testGood(){ + UndoManager u = new UndoManager(); + u.addEdit(null); + u.redo(); + u.setLimit(10); + u.redo(); + u.end(); + u.undoOrRedo(); + } + + void test2(){ + UndoManager u = new UndoManager(); + u.undo(); + u.addEdit(null); + } + + void test3(){ + UndoManager u = new UndoManager(); + u.undoableEditHappened(null); + u.undo(); + u.end(); + u.setLimit(100);//error + } +} \ No newline at end of file diff --git a/examples/demo/src/main/java/com/undomanager/UndoManagerRefinements.java b/examples/demo/src/main/java/com/undomanager/UndoManagerRefinements.java new file mode 100644 index 0000000..64825d6 --- /dev/null +++ b/examples/demo/src/main/java/com/undomanager/UndoManagerRefinements.java @@ -0,0 +1,68 @@ +package com.undomanager; + +import javax.swing.event.UndoableEditEvent; +import javax.swing.undo.UndoableEdit; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@ExternalRefinementsFor("javax.swing.undo.UndoManager") +@StateSet({"start", "canEdit", "end"}) +public interface UndoManagerRefinements { + + @StateRefinement(to="start(this)") + void UndoManager(); + + @StateRefinement(from="start(this)", to="canEdit(this)") + boolean addEdit(UndoableEdit anEdit); + + @StateRefinement(from="canEdit(this)") + void discardAllEdits(); + + @StateRefinement(to="end(this)") + void end(); + + @StateRefinement(from="canEdit(this)") + @StateRefinement(from="end(this)") + String getRedoPresentationName(); + + @StateRefinement(from="canEdit(this)") + @StateRefinement(from="end(this)") + String getUndoOrRedoPresentationName(); + + @StateRefinement(from="canEdit(this)") + @StateRefinement(from="end(this)") + String getUndoPresentationName(); + + @StateRefinement(from="canEdit(this)") + @StateRefinement(from="end(this)") + void redo(); + + @StateRefinement(from="start(this)") + @StateRefinement(from="canEdit(this)") + void setLimit(int l); + + @StateRefinement(from="canEdit(this)") + @StateRefinement(from="end(this)") + void undo(); + + @StateRefinement(from="start(this)", to="canEdit(this)") + @StateRefinement(from="canEdit(this)") + @StateRefinement(from="end(this)") + void undoableEditHappened(UndoableEditEvent e); + + @StateRefinement(from="canEdit(this)") + @StateRefinement(from="end(this)") + void undoOrRedo(); + + + + // int getLimit(); //any + // boolean canRedo(); + + // boolean canUndo(); + + // boolean canUndoOrRedo(); + +} diff --git a/examples/demo/src/main/java/com/uuid/Test.java b/examples/demo/src/main/java/com/uuid/Test.java new file mode 100644 index 0000000..f49d945 --- /dev/null +++ b/examples/demo/src/main/java/com/uuid/Test.java @@ -0,0 +1,48 @@ +package com.uuid; + +import java.util.UUID; + +public class Test { + + void test1(){ + long mostSigBits = 0x0000000000001000; + UUID t = new UUID(mostSigBits, 0L); + t.clockSequence(); // possible + } + + void test2(){ + long mostSigBits = 0x0670034000001222L; + UUID t = new UUID(mostSigBits, 0L); + t.clockSequence(); // possible + } + + void test3(){ + UUID t = UUID.randomUUID(); + t.clockSequence(); //error + } + + void test4(){ + UUID t = UUID.fromString("smt"); + t.clockSequence(); //possible + t.node(); + t.variant(); + } + + void test5(){ + byte[] bytes = {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0}; + UUID t = UUID.nameUUIDFromBytes(bytes); + t.variant(); + t.version(); + t.timestamp();//error + + } + + + void test6(){ + long mostSigBits = 0x0000000000002000; + UUID t = new UUID(mostSigBits, 0L); + t.clockSequence(); // error + } + + +} diff --git a/examples/demo/src/main/java/com/uuid/UUIDRefinements.java b/examples/demo/src/main/java/com/uuid/UUIDRefinements.java new file mode 100644 index 0000000..edf7764 --- /dev/null +++ b/examples/demo/src/main/java/com/uuid/UUIDRefinements.java @@ -0,0 +1,60 @@ +package com.uuid; + +import java.util.UUID; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.Refinement; +import liquidjava.specification.RefinementAlias; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; +// 0x000000000000F000 +// (v/4096) % 16; + +@ExternalRefinementsFor("java.util.UUID") +@StateSet({"other", "maybeTime", "timeBased"}) +@RefinementAlias("Version(int v) {v >= 0 && v <= 4}") +@RefinementAlias("Variant(int v) {v == 0 || v == 2 || v == 6 || v == 7}") +public interface UUIDRefinements { + + // creation + @StateRefinement(to="((mostSigBits/4096) % 16 == 1) ? timeBased(this) : other(this)") + void UUID(long mostSigBits, long leastSigBits); + + //static + @Refinement("maybeTime(return)") + UUID fromString(String name); + + //static + @Refinement("other(return)") + UUID nameUUIDFromBytes(byte[] name); + + //static + @Refinement("other(return)") + UUID randomUUID(); + + + @StateRefinement(from="maybeTime(this)") + @StateRefinement(from="timeBased(this)") + int clockSequence(); + + @StateRefinement(from="maybeTime(this)") + @StateRefinement(from="timeBased(this)") + long timestamp(); + + @StateRefinement(from="maybeTime(this)") + @StateRefinement(from="timeBased(this)") + long node(); + + @Refinement("Variant(_)") + int variant(); + @Refinement("Version(_)") + int version(); + + // int compareTo(UUID val); + // boolean equals(Object obj); + // long getLeastSignificantBits(); + // long getMostSignificantBits(); + // int hashCode(); + // String toString(); + +} diff --git a/examples/demo/src/main/java/com/window/TestWindows.java b/examples/demo/src/main/java/com/window/TestWindows.java new file mode 100644 index 0000000..a80ba5b --- /dev/null +++ b/examples/demo/src/main/java/com/window/TestWindows.java @@ -0,0 +1,32 @@ +package com.window; + +import java.awt.Window; + +public class TestWindows { + void test1(){ + Window w = new Window(null); + w.pack(); + w.setType(Window.Type.NORMAL); + } + + void test2(){ + Window w = new Window(null); + w.setType(Window.Type.NORMAL); + w.setVisible(false); + w.createBufferStrategy(1); + } + + void test3(){ + Window w = new Window(null); + w.setType(Window.Type.NORMAL); + w.setVisible(true); + w.dispose(); + w.createBufferStrategy(1); + } + + void test4(){ + Window w = new Window(null); + w.pack(); + w.setType(Window.Type.NORMAL); + } +} diff --git a/examples/demo/src/main/java/com/window/WindowRefinements.java b/examples/demo/src/main/java/com/window/WindowRefinements.java new file mode 100644 index 0000000..80a9e39 --- /dev/null +++ b/examples/demo/src/main/java/com/window/WindowRefinements.java @@ -0,0 +1,59 @@ +package com.window; + +import java.awt.AWTKeyStroke; +import java.awt.BufferCapabilities; +import java.awt.Frame; +import java.awt.GraphicsConfiguration; +import java.awt.Window; +import java.util.Set; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.Refinement; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"displayable", "notDisplayable"}) +@ExternalRefinementsFor("java.awt.Window") +public interface WindowRefinements{ + + @StateRefinement(to="notDisplayable(this)") + void Window(Frame owner); + + @StateRefinement(to="notDisplayable(this)") + void Window(Window owner); + + @StateRefinement(to="notDisplayable(this)") + void Window(Window owner, GraphicsConfiguration gc); + + + // to displayable + @StateRefinement(to="displayable(this)") + void addNotify(); // Makes this Window displayable by creating the connection to its native screen resource. This method is called internally by the toolkit and should not be called directly by programs. + + @StateRefinement(to="displayable(this)") + void pack(); //If the window and/or its owner are not displayable yet, both of them are made displayable + + @StateRefinement(from="notDisplayable(this)") + @StateRefinement(from="notDisplayable(this) && b",to="displayable(this)") // if its not displayable yet, is made displayable + @StateRefinement(from="displayable(this)") // stays displayable + void setVisible(boolean b); + + + @StateRefinement(to="notDisplayable(this)") + void dispose(); // makes not displayable. It can be displayed again later by calling pack(). + + @StateRefinement(from="displayable(this)") + void createBufferStrategy(@Refinement("_ > 0")int numBuffers);// IllegalStateException - if the component is not displayable + + + void createBufferStrategy(@Refinement("_ > 0") int numBuffers, BufferCapabilities caps); + + @StateRefinement(from="notDisplayable(this)") + void setType(Window.Type type); // Sets the type of the window. This method can only be called while the window is not displayable. + + + Set getFocusTraversalKeys(@Refinement("_ >= 0 && _ <= 3") int id); + + void setOpacity(@Refinement("_ >= 0 && _ <= 1") float opacity); + +}