diff --git a/examples/demo/src/main/java/com/example/abstractundoableedit/AbstractUndoableEditRefinements.java b/examples/demo/src/main/java/com/example/abstractundoableedit/AbstractUndoableEditRefinements.java
new file mode 100644
index 0000000..c8d096d
--- /dev/null
+++ b/examples/demo/src/main/java/com/example/abstractundoableedit/AbstractUndoableEditRefinements.java
@@ -0,0 +1,47 @@
+package com.example.abstractundoableedit;
+
+import javax.swing.undo.CannotUndoException;
+import javax.swing.undo.UndoableEdit;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.Refinement;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@ExternalRefinementsFor("javax.swing.undo.AbstractUndoableEdit")
+@StateSet({"alive_done", "not_alive_done", "alive_not_done", "not_alive_not_done"})
+public interface AbstractUndoableEditRefinements {
+    @StateRefinement(to="alive_done(this)")
+    public void AbstractUndoableEdit();
+
+    @StateRefinement(from="alive_done(this)", to="not_alive_done(this)")
+    @StateRefinement(from="alive_not_done(this)", to="not_alive_not_done(this)")
+    public void die();
+
+
+    @StateRefinement(from="alive_done(this)", to="alive_not_done(this)")
+    public void undo() throws CannotUndoException;
+
+    @Refinement("_ && alive_done(this) || !_ && !alive_done(this)")
+    public boolean canUndo();
+
+    @StateRefinement(from="alive_not_done(this)", to="alive_done(this)")
+    public void redo() throws CannotUndoException;
+
+    @Refinement("_ && alive_not_done(this) || !_ && !alive_not_done(this)")
+    public boolean canRedo();
+
+    public boolean addEdit(UndoableEdit anEdit);
+
+    public boolean replaceEdit(UndoableEdit anEdit);
+
+    public boolean isSignificant();
+
+    public String getPresentationName();
+
+    public String getUndoPresentationName();
+
+    public String getRedoPresentationName();
+
+    public String toString();
+}
diff --git a/examples/demo/src/main/java/com/example/abstractundoableedit/AbstractUndoableEditTest.java b/examples/demo/src/main/java/com/example/abstractundoableedit/AbstractUndoableEditTest.java
new file mode 100644
index 0000000..aa4e8be
--- /dev/null
+++ b/examples/demo/src/main/java/com/example/abstractundoableedit/AbstractUndoableEditTest.java
@@ -0,0 +1,31 @@
+package com.example.abstractundoableedit;
+
+import javax.swing.undo.AbstractUndoableEdit;
+
+public class AbstractUndoableEditTest {
+    void test1() {
+        AbstractUndoableEdit a = new AbstractUndoableEdit();
+        //a.die(); // if commented in, LiquidJava should report an error on the next line
+        a.undo();
+        a.redo();
+        a.die();
+    }
+
+    void test4() {
+        AbstractUndoableEdit a = new AbstractUndoableEdit();
+        a.undo();
+        a.die();
+    }
+
+    void test2(AbstractUndoableEdit a) {
+        if (a.canUndo()) {
+            a.undo();
+            a.redo();
+        }
+    }
+    void test3(AbstractUndoableEdit a) {
+        if (a.canRedo()) {
+            a.redo();
+        }
+    }
+}
diff --git a/examples/demo/src/main/java/com/example/pipedwriter/PipedWriterRefinements.java b/examples/demo/src/main/java/com/example/pipedwriter/PipedWriterRefinements.java
new file mode 100644
index 0000000..a338ef7
--- /dev/null
+++ b/examples/demo/src/main/java/com/example/pipedwriter/PipedWriterRefinements.java
@@ -0,0 +1,43 @@
+package com.example.pipedwriter;
+
+import java.io.IOException;
+import java.io.PipedReader;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.Refinement;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@ExternalRefinementsFor("java.io.PipedWriter")
+//@RefinementAlias("Index(int x) {x >= 0}")
+@StateSet({"unconnected", "connected", "broken", "closed"})
+public interface PipedWriterRefinements {
+    @StateRefinement(to="connected(this)")
+    public void PipedWriter(PipedReader snk)
+                throws IOException;
+
+    @StateRefinement(to="unconnected(this)")
+    public void PipedWriter();
+
+    @StateRefinement(from="unconnected(this)", to="connected(this)")
+    public void connect(PipedReader snk)
+             throws IOException;
+
+    @StateRefinement(from="connected(this)")
+    public void write(@Refinement("c >= 0 && c <= 65535") int c)
+           throws IOException;
+
+    @StateRefinement(from="connected(this)")
+    public void write(char[] cbuf,
+                        @Refinement("off >= 0") int off,
+                        @Refinement("off >= 0") int len)
+           throws IOException;
+
+    @StateRefinement(from="connected(this)")
+    public void flush()
+           throws IOException;
+
+    @StateRefinement(to="closed(this)")
+    public void close()
+           throws IOException;
+}
diff --git a/examples/demo/src/main/java/com/example/pipedwriter/PipedWriterTest.java b/examples/demo/src/main/java/com/example/pipedwriter/PipedWriterTest.java
new file mode 100644
index 0000000..561b17e
--- /dev/null
+++ b/examples/demo/src/main/java/com/example/pipedwriter/PipedWriterTest.java
@@ -0,0 +1,35 @@
+package com.example.pipedwriter;
+
+import java.io.IOException;
+import java.io.PipedReader;
+import java.io.PipedWriter;
+
+public class PipedWriterTest {
+    void test1() throws IOException {
+        PipedWriter p = new PipedWriter();
+        PipedReader r = new PipedReader();
+        p.connect(r);
+        p.write('a');
+        p.flush();
+        p.close();
+        r.close();
+    }
+    void test2() throws IOException {
+        PipedReader r = new PipedReader();
+        PipedWriter p = new PipedWriter(r);
+        char [] arr = {'a', 'b', 'c'};
+        p.write(arr, 1, 2);
+        p.flush();
+        p.close();
+        r.close();
+    }
+    void testFail() throws IOException {
+        PipedWriter p = new PipedWriter();
+        PipedReader r = new PipedReader();
+        p.flush();
+        char [] arr = {'a', 'b', 'c'};
+        p.write(arr, 2, 2);
+        p.close();
+        r.close();
+    }
+}