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..669995d
--- /dev/null
+++ b/examples/demo/src/main/java/com/example/pipedwriter/PipedWriterTest.java
@@ -0,0 +1,38 @@
+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'*/35);
+        p.flush();
+        p.close();
+        r.close();
+    }
+    void test2() throws IOException {
+        PipedReader r = new PipedReader();
+        PipedWriter p = new PipedWriter(r);
+        char [] arr = {}; // OK for LiquidJava
+        // char c = 'a';  // breaks LiquidJava
+
+        p.write(arr, 1, 2);
+        p.flush();
+        p.close();
+        r.close();
+    }
+    void testFail() throws IOException {
+        PipedWriter p = new PipedWriter();
+        PipedReader r = new PipedReader();
+        //char [] arr = {'a', 'b', 'c'}; // breaks LiquidJava
+        p.flush();
+        char [] arr2 = {'a', 'b', 'c'}; // breaks LiquidJava if analyzed (it isn't here, because there's an error in p.flush() above)
+        p.write(arr2, 2, 2);
+        p.close();
+        r.close();
+    }
+}
diff --git a/examples/demo/src/main/java/com/example/uuid/UUIDRefinements.java b/examples/demo/src/main/java/com/example/uuid/UUIDRefinements.java
new file mode 100644
index 0000000..3b2a6fb
--- /dev/null
+++ b/examples/demo/src/main/java/com/example/uuid/UUIDRefinements.java
@@ -0,0 +1,34 @@
+package com.example.uuid;
+
+import java.util.UUID;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.Refinement;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@ExternalRefinementsFor("java.util.UUID")
+@StateSet({"time_based", "dce_security", "name_based", "random"})
+public interface UUIDRefinements {
+    //@StateRefinement(from="leastSigBits & 0xC000000000000000 == 0xB000000000000000 && mostSigBits & 0x000000000000F000 == 0x0000000000001000", to="time_based(this)")
+    public void UUID(long mostSigBits, long leastSigBits);
+
+    // QUESTION: is this how static methods should be specified?
+    @Refinement("random(_)")
+    public UUID randomUUID();
+
+    @Refinement("name_based(_)")
+    public UUID nameUUIDFromBytes(byte[] name);
+
+    @Refinement("_ == 1 && time_based(this) || _ == 2 && dce_security(this) || _ == 3 && name_based(this) || _ == 4 && random(this)")
+    public int version();
+
+    @StateRefinement(from="time_based(this)")
+    public long timestamp();
+
+    @StateRefinement(from="time_based(this)")
+    public int clockSequence();
+
+    @StateRefinement(from="time_based(this)")
+    public long node();
+}
diff --git a/examples/demo/src/main/java/com/example/uuid/UUIDTest.java b/examples/demo/src/main/java/com/example/uuid/UUIDTest.java
new file mode 100644
index 0000000..55b4364
--- /dev/null
+++ b/examples/demo/src/main/java/com/example/uuid/UUIDTest.java
@@ -0,0 +1,23 @@
+package com.example.uuid;
+
+import java.util.UUID;
+
+public class UUIDTest {
+    void test1fail() {
+        UUID u = UUID.randomUUID();
+        u.timestamp(); // should report an error, because u is not time-based
+    }
+    void test2fail(UUID u) {
+        u.clockSequence(); // should report an error, because u may not be time-based
+    }
+    void test3(UUID u) {
+        if (u.version() == 1) {
+            u.node(); // should be OK, because u is time-based
+        }
+    }
+    void test4fail(UUID u) {
+        if (u.version() == 2) {
+            u.timestamp(); // should report an error, because u is not time-based -- but I don't get an error.
+        }
+    }
+}