1 files changed, 0 insertions, 132 deletions
diff --git a/Chalice/tests/examples/HandOverHand.chalice b/Chalice/tests/examples/HandOverHand.chalice
deleted file mode 100644
index 31818ca6..00000000
--- a/Chalice/tests/examples/HandOverHand.chalice
+++ /dev/null
@@ -1,132 +0,0 @@
-class List {
-  ghost var sum: int
-  var head: Node
-  invariant acc(head) && head != null
-  invariant rd(head.val) && head.val == -1
-  invariant rd(mu) && acc(head.mu,50) && this << head
-  invariant acc(sum,20) && acc(head.sum, 50) && sum == head.sum
-
-  method Main()
-  {
-    var list := new List
-    call list.Init()
-    call list.Insert(8)
-    call list.Insert(12)
-    call list.Insert(4)
-    assert list.sum == 24
-  }
-
-  method Init()
-    requires acc(mu) && mu == lockbottom && acc(head) && acc(sum)
-    ensures rd*(mu) && waitlevel << this
-    ensures acc(sum,80) && sum == 0
-  {
-    var t := new Node
-    t.val := -1
-    t.next := null
-    t.sum := 0
-    share t
-    head := t
-    sum := 0
-    share this between waitlevel and t
-  }
-
-  method Insert(x: int)
-    requires rd(mu) && waitlevel << this
-    requires acc(sum,80) && 0 <= x
-    ensures rd(mu)
-    ensures acc(sum,80) && sum == old(sum) + x
-  {
-    acquire this
-    assert waitlevel == this.mu;
-    sum := sum + x
-    var p: Node := head
-    acquire p
-    p.sum := p.sum + x
-    release this
-
-    while (p.next != null && p.next.val < x)
-      invariant p != null && acc(p.next) && acc(p.val,rd(p)) && acc(p.mu,50)
-      invariant holds(p) && waitlevel == p.mu
-      invariant !old(holds(p)) && !old(rd holds(p))
-      invariant p.next != null ==> acc(p.next.mu,50) && p << p.next
-      invariant p.next != null ==> acc(p.next.val,rd(p.next)) && p.val <= p.next.val
-      invariant acc(p.sum, 50)
-      invariant p.next == null ==> p.sum == x
-      invariant p.next != null ==> acc(p.next.sum, 50) && p.sum == p.next.val + p.next.sum + x
-      invariant p.val <= x
-      lockchange p
-    {
-      var nx: Node := p.next
-      acquire nx
-      nx.sum := nx.sum + x
-      release p
-      p := nx
-    }
-    var t := new Node
-    t.val := x
-    t.next := p.next
-    if (t.next == null) { t.sum := 0 } else { t.sum := p.next.val + p.next.sum }
-    share t between p and p.next
-    p.next := t
-    release p
-  }
-
-  method Delete(x: int) returns (wasPresent: bool)
-    requires rd(mu) && waitlevel << this
-    requires acc(sum,80) && 0 <= x
-    ensures acc(sum,80) && (wasPresent ==> sum == old(sum) - x) && (!wasPresent ==> sum == old(sum))
-  {
-    ghost const c
-
-    acquire this
-    sum := sum - c
-    var p: Node := head
-    acquire p
-    p.sum := p.sum - c
-    release this
-
-    while (p.next != null && p.next.val < x)
-      invariant p != null && acc(p.next) && acc(p.val,rd(p)) && acc(p.mu,50)
-      invariant holds(p) && waitlevel == p.mu && !assigned(c)
-      invariant !old(holds(p)) && !old(rd holds(p))
-      invariant p.next != null ==> acc(p.next.mu,50) && p << p.next
-      invariant p.next != null ==> acc(p.next.val,rd(p.next)) && p.val <= p.next.val
-      invariant acc(p.sum, 50)
-      invariant p.next == null ==> p.sum == 0 - c
-      invariant p.next != null ==> acc(p.next.sum, 50) && p.sum == p.next.val + p.next.sum - c
-      invariant p.val <= x
-      lockchange p
-    {
-      var nx: Node := p.next
-      acquire nx
-      nx.sum := nx.sum - c
-      release p
-      p := nx
-    }
-    if (p.next != null && p.next.val == x) {
-      wasPresent := true
-      c := x
-      var nx: Node := p.next
-      acquire nx
-      p.next := nx.next
-      unshare nx
-    } else {
-      wasPresent := false
-      c := 0
-    }
-    release p
-  }
-}
-
-class Node {
-  ghost var sum: int
-  var val: int
-  var next: Node
-  invariant acc(next) && rd(val)
-  invariant next != null ==> rd(next.val) && val <= next.val
-  invariant acc(sum, 50)
-  invariant next == null ==> sum == 0
-  invariant next != null ==> acc(next.sum, 50) && sum == next.val + next.sum
-  invariant acc(mu,50) && (next != null ==> acc(next.mu,50) && this << next)
-}