1 files changed, 152 insertions, 0 deletions
diff --git a/Chalice/tests/examples/counter.chalice b/Chalice/tests/examples/counter.chalice
new file mode 100644
index 00000000..828cf005
--- /dev/null
+++ b/Chalice/tests/examples/counter.chalice
@@ -0,0 +1,152 @@
+class Counter {
+  var value: int;
+
+  invariant acc(value) && old(value)<=value;
+}
+
+class Program {
+
+  method main1(){
+    var counter := new Counter;
+    counter.value := 0;
+    share counter;
+
+    acquire counter;
+    var tmp1 := counter.value;
+    release counter;
+    
+    acquire counter;
+    var tmp2 := counter.value;
+    release counter;
+
+    assert tmp1 <= tmp2;
+  }
+
+  method main2(){
+    var counter := new Counter;
+    counter.value := 0;
+    share counter;
+
+    acquire counter;
+    release counter;
+
+    call bar(counter);
+  }
+
+  method bar(c: Counter)
+    requires c!=null && acc(c.mu) && waitlevel << c.mu;
+    requires eval(c.release, acc(c.value) && 0<=c.value);
+  {
+    lock (c) {
+      assert 0 <= c.value; // ok, because of the lastSeen conjunct in the precondition
+    }
+  }
+
+  method main3() returns (counter: Counter)
+    lockchange counter;
+  {
+    counter := new Counter;
+    counter.value := 0;
+    share counter;
+    acquire counter;
+    call doRelease(counter, counter.value);
+  }
+
+  method doRelease(c: Counter, i: int)
+    requires c!=null && holds(c) && acc(c.value) && eval(c.acquire, acc(c.value) && i<=c.value);
+    lockchange c;
+  {
+    release c; // ok, because of atAcquire conjunct in the precondition
+  }
+
+  method main4(){
+    var counter := new Counter;
+    counter.value := 0;
+    share counter;
+
+    acquire counter;
+    counter.value := counter.value - 1;
+    release counter;  // error: should fail
+  }
+
+  method main5(){
+    var counter := new Counter;
+    counter.value := 10;
+    share counter;
+
+    call foo(counter);
+
+    unshare counter;
+    assert 10<=counter.value; // error: should fail
+  }
+
+  method foo(c: Counter)
+    requires c!=null && acc(c.mu) && waitlevel << c.mu && eval(c.release, acc(c.value) && 10<=c.value);
+    ensures c!=null && holds(c) && acc(c.mu) && acc(c.value);
+    lockchange c;
+  {
+    acquire c;
+    unshare c;
+    c.value := 5;
+    share c;
+    acquire c;
+  }
+
+  method nestedGood0(c: Counter)
+    requires c != null && acc(c.mu) && waitlevel << c.mu;
+  {
+    lock (c) {
+      release c
+      acquire c
+    }
+  }
+
+  method nestedGood1(c: Counter)
+    requires c != null && acc(c.mu) && waitlevel << c.mu;
+  {
+    var t: Counter := c
+    lock (t) {
+      t := new Counter
+      share t
+      acquire t
+    }  // this line releases the original value for t
+    release t
+  }
+
+  method nestedBad0(c: Counter)
+    requires c != null && acc(c.mu) && waitlevel << c.mu;
+  {
+    lock (c) {
+      release c
+    }  // error: no longer holds c
+  }
+
+  method nestedBad1(c: Counter)
+    requires c != null && acc(c.mu) && waitlevel << c.mu;
+  {
+    lock (c) {
+      acquire c  // error: already holds c
+    }
+  }
+
+  method nestedBad2(c: Counter)
+    requires c != null && acc(c.mu) && waitlevel << c.mu;
+  {
+    lock (c) {
+      lock (c) {  // error: already holds c
+      }
+    }
+  }
+
+  method nestedBad3(c: Counter)
+    requires c != null && acc(c.mu) && waitlevel << c.mu;
+  {
+    var t: Counter := c
+    lock (t) {
+      release t
+      t := new Counter
+      share t
+      acquire t
+    }  // error: this line attempts to release the original t
+  }
+}
+\ No newline at end of file