1 files changed, 113 insertions, 0 deletions
diff --git a/Chalice/tests/examples/AssociationList.chalice b/Chalice/tests/examples/AssociationList.chalice
new file mode 100644
index 00000000..cc3ecfb4
--- /dev/null
+++ b/Chalice/tests/examples/AssociationList.chalice
@@ -0,0 +1,113 @@
+class Client {
+  method Main(d: Data)
+    requires d != null
+  {
+    var a := new AssociationList
+    call a.Init()
+    call a.Add(5, d)
+    call a.Add(10, d)
+    var t: Data
+    call t := a.Get(10)
+  }
+}
+
+class AssociationList {
+  var head: Node  // sentinel
+  invariant rd(head) && head != null
+  invariant rd(mu) && rd(head.mu) && this << head
+
+  method Init()
+    requires acc(head) && acc(mu) && mu == lockbottom
+    ensures acc(mu) && waitlevel << this
+  {
+    head := new Node
+    head.next := null
+    share head
+    share this between waitlevel and head
+  }
+
+  method Add(key: int, value: Data)
+    requires value != null
+    requires rd(mu) && waitlevel << this
+    ensures rd(mu)
+  {
+    acquire this
+    var p: Node := head
+    acquire p
+    release this
+
+    var n := new Node
+    n.key := key
+    n.value := value
+    n.next := p.next
+    p.next := n
+    share n between p and n.next
+    release p
+  }
+
+  method Get(key: int) returns (d: Data)
+    requires rd(mu) && waitlevel << this
+    ensures rd(mu)
+  {
+    d := null
+    acquire this
+    var p: Node := head
+    acquire p
+    release this
+
+    if (p.next != null) {
+      acquire p.next
+      if (p.next.key == key) {
+        d := p.next.value
+      } else {
+        var done := false
+        while (!done)
+          // invariant:  holds p and p.next
+          invariant p != null && rd(p.key) && rd(p.value) && acc(p.next) && acc(p.mu,50) && p.next != null
+          invariant acc(p.next.mu) && p << p.next
+          invariant rd(p.next.key) && rd(p.next.value) && acc(p.next.next)
+          invariant p.next.next != null ==>
+              acc(p.next.next.mu,50) && p.next << p.next.next
+          invariant holds(p) && holds(p.next) && waitlevel == p.next.mu
+          invariant p.next.next != null ==> waitlevel << p.next.next
+          lockchange p, p.next.next
+        {
+          if (p.next.next == null) {
+            done := true  // key not present
+          } else {
+            acquire p.next.next
+            if (p.next.next.key == key) {
+              done := true  // key is present
+              d := p.next.next.value
+              // move p.next.next closer to the head by one step
+
+              var t: Node := p.next
+              p.next := t.next
+              t.next := p.next.next
+              p.next.next := t
+              reorder t between p.next and t.next
+              release t
+            } else {
+              var t: Node := p
+              p := p.next
+              release t
+            }
+          }
+        }
+      }
+      release p.next
+    }
+    release p
+  }
+}
+
+class Data { }
+
+class Node
+{
+  var key: int
+  var value: Data
+  var next: Node
+  invariant rd(key) && rd(value) && acc(next) && acc(mu,50)
+  invariant next != null ==> acc(next.mu,50) && this << next
+}