1 files changed, 0 insertions, 122 deletions
diff --git a/Chalice/tests/examples/AssociationList.chalice b/Chalice/tests/examples/AssociationList.chalice
deleted file mode 100644
index 418bcd12..00000000
--- a/Chalice/tests/examples/AssociationList.chalice
+++ /dev/null
@@ -1,122 +0,0 @@
-/*
-  Note: This example seems to be completely broken. The failing assertion
-  about locking/unlocking too much causes an inconsistency and all following
-  assertions pass by default.
-  It seems that the specification, in particular the loop invariant in method
-  Add, is wrong. (see also http://boogie.codeplex.com/workitem/10207)
-  -- August 2011, Stefan Heule
-*/
-
-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
-}