Initial set of files.

21 files changed, 2479 insertions, 0 deletions

diff --git a/Chalice/examples/Answer b/Chalice/examples/Answer
new file mode 100644
index 00000000..b81e3893
--- /dev/null
+++ b/Chalice/examples/Answer
@@ -0,0 +1,235 @@
+start 

+------ Running regression test AssociationList.chalice 

+

+Boogie program verifier finished with 12 verified, 0 errors

+------ Running regression test cell.chalice 

+  142.5: Assertion might not hold. Insufficient fraction at 142.12 for Cell.valid.

+

+Boogie program verifier finished with 31 verified, 1 error

+------ Running regression test counter.chalice 

+  69.5: Monitor invariant might hot hold. The expression at 4.27 might not evaluate to true.

+  80.5: Assertion might not hold. The expression at 80.12 might not evaluate to true.

+  119.5: The held field of the target of the release statement might not be writable.

+  128.7: The mu field of the target of the acquire statement might not be above maxlock.

+  136.7: The mu field of the target of the acquire statement might not be above maxlock.

+  145.5: The held field of the target of the release statement might not be writable.

+

+Boogie program verifier finished with 24 verified, 6 errors

+------ Running regression test dining-philosophers.chalice 

+

+Boogie program verifier finished with 12 verified, 0 errors

+------ Running regression test ForkJoin.chalice 

+

+Boogie program verifier finished with 18 verified, 0 errors

+------ Running regression test HandOverHand.chalice 

+

+Boogie program verifier finished with 10 verified, 0 errors

+------ Running regression test iterator.chalice 

+

+Boogie program verifier finished with 22 verified, 0 errors

+------ Running regression test iterator2.chalice 

+

+Boogie program verifier finished with 21 verified, 0 errors

+------ Running regression test producer-consumer.chalice 

+

+Boogie program verifier finished with 36 verified, 0 errors

+------ Running regression test prog0.chalice 

+The program did not typecheck.

+3.17: undeclared member a in class C

+3.37: undeclared member a in class C

+3.41: undeclared member a in class C

+3.12: assert statement requires a boolean expression (found int)

+4.5: undeclared member a in class C

+4.10: undeclared member a in class C

+5.5: undeclared member b in class C

+5.10: undeclared member a in class C

+5.14: undeclared member b in class C

+5.18: undeclared member c in class C

+5.26: undeclared member d in class C

+6.5: undeclared member b in class C

+6.14: undeclared member a in class C

+6.18: undeclared member b in class C

+6.23: undeclared member c in class C

+6.32: undeclared member d in class C

+7.5: undeclared member c in class C

+7.10: undeclared member a in class C

+7.15: undeclared member b in class C

+7.20: undeclared member c in class C

+7.29: undeclared member d in class C

+8.13: undeclared member X in class C

+8.19: undeclared member Y in class C

+8.13: incorrect type of ==> LHS (expected bool, found int)

+8.19: incorrect type of ==> RHS (expected bool, found int)

+8.26: undeclared member Z in class C

+8.26: incorrect type of ==> RHS (expected bool, found int)

+8.33: undeclared member A in class C

+8.39: undeclared member B in class C

+8.45: undeclared member C in class C

+8.39: incorrect type of ==> LHS (expected bool, found int)

+8.45: incorrect type of ==> RHS (expected bool, found int)

+8.33: incorrect type of ==> LHS (expected bool, found int)

+9.12: undeclared member A in class C

+9.17: undeclared member B in class C

+9.12: incorrect type of && LHS (expected bool, found int)

+9.17: incorrect type of && RHS (expected bool, found int)

+9.23: undeclared member C in class C

+9.28: undeclared member D in class C

+9.23: incorrect type of || LHS (expected bool, found int)

+9.28: incorrect type of || RHS (expected bool, found int)

+9.33: undeclared member E in class C

+9.33: incorrect type of || RHS (expected bool, found int)

+9.39: undeclared member F in class C

+9.39: incorrect type of && RHS (expected bool, found int)

+11.21: undeclared member f in class int

+11.21: undeclared member g in class int

+11.21: undeclared member h in class int

+<undefined position>: not-expression requires boolean operand

+<undefined position>: incorrect type of + RHS (expected int, found bool)

+11.33: not-expression requires boolean operand

+11.33: undeclared member f in class bool

+11.43: undeclared member f in class int

+11.42: not-expression requires boolean operand

+11.42: incorrect type of + RHS (expected int, found bool)

+13.5: type mismatch in assignment, lhs=int rhs=D

+14.5: undeclared member o in class C

+14.5: undeclared member f in class int

+15.6: undeclared member a in class C

+15.10: undeclared member b in class C

+15.5: undeclared member y in class int

+15.18: undefined class T used in new expression

+16.19: undeclared member O in class C

+16.14: == requires operands of the same type, found int and bool

+16.31: undeclared member O in class C

+16.13: != requires operands of the same type, found bool and int

+16.13: object in install statement must be of a reference type (found bool)

+16.41: undeclared member a in class C

+16.41: install bound must be of a reference type or Mu type (found int)

+16.43: undeclared member b in class C

+16.43: install bound must be of a reference type or Mu type (found int)

+16.45: undeclared member c in class C

+16.45: install bound must be of a reference type or Mu type (found int)

+16.51: install bound must be of a reference type or Mu type (found int)

+16.53: install bound must be of a reference type or Mu type (found int)

+17.13: undeclared member X in class C

+17.19: undeclared member Y in class C

+17.13: incorrect type of ==> LHS (expected bool, found int)

+17.19: incorrect type of ==> RHS (expected bool, found int)

+17.13: object in install statement must be of a reference type (found bool)

+17.27: install bound must be of a reference type or Mu type (found int)

+18.13: undeclared member o in class C

+18.13: undeclared member f in class int

+18.13: object in install statement must be of a reference type (found int)

+19.11: undeclared member o in class C

+19.11: object in share statement must be of a reference type (found int)

+20.13: undeclared member o in class C

+20.13: object in unshare statement must be of a reference type (found int)

+21.13: undeclared member o in class C

+21.13: object in acquire statement must be of a reference type (found int)

+22.13: undeclared member o in class C

+22.13: object in release statement must be of a reference type (found int)

+23.16: undeclared member o in class C

+23.16: object in rd acquire statement must be of a reference type (found int)

+24.16: undeclared member o in class C

+24.16: object in rd release statement must be of a reference type (found int)

+25.15: undeclared member o in class C

+25.15: object in downgrade statement must be of a reference type (found int)

+27.17: undeclared member o in class C

+27.5: call of undeclared member m in class int

+27.10: wrong token type

+29.12: rd expression is allowed only in positive predicate contexts

+29.15: undeclared member x in class C

+29.20: acc expression is allowed only in positive predicate contexts

+29.24: undeclared member y in class C

+29.12: incorrect type of + LHS (expected int, found bool)

+29.20: incorrect type of + RHS (expected int, found bool)

+29.29: acc expression is allowed only in positive predicate contexts

+29.33: undeclared member z in class C

+29.29: incorrect type of + RHS (expected int, found bool)

+29.51: undeclared member k in class C

+29.57: undeclared member f in class null

+29.12: assert statement requires a boolean expression (found int)

+30.10: undeclared member f in class C

+31.5: wrong number of actual in-parameters in call to C.m (3 instead of 0)

+32.5: wrong number of actual in-parameters in call to C.m (3 instead of 0)

+33.19: undeclared member o in class C

+33.10: undefined local variable a

+33.12: undefined local variable b

+33.14: undefined local variable c

+33.5: call of undeclared member m in class int

+34.5: wrong number of actual in-parameters in call to C.m (1 instead of 0)

+34.5: wrong number of actual out-parameters in call to C.m (1 instead of 0)

+35.13: undeclared member o in class C

+35.13: object in install statement must be of a reference type (found int)

+58.17: undeclared member sqrt2 in class C

+58.25: undeclared member sqrt2 in class C

+62.17: undeclared member s in class C

+62.10: undefined local variable v

+62.5: call of undeclared member M in class int

+------ Running regression test prog1.chalice 

+  9.10: Location might not be readable.

+  25.5: Location might not be writable

+  33.14: Location might not be readable.

+  42.5: Monitor invariant might hot hold. The expression at 5.23 might not evaluate to true.

+  60.5: Location might not be writable

+  76.5: The held field of the target of the unshare statement might not be writable.

+  84.5: The held field of the target of the unshare statement might not be writable.

+

+Boogie program verifier finished with 16 verified, 7 errors

+------ Running regression test prog2.chalice 

+  24.5: Assertion might not hold. The expression at 24.12 might not evaluate to true.

+  31.13: Location might not be readable.

+  73.5: Const variable can be assigned to only once.

+  78.5: Assertion might not hold. The expression at 78.12 might not evaluate to true.

+

+Boogie program verifier finished with 24 verified, 4 errors

+------ Running regression test prog3.chalice 

+  76.3: The postcondition at 77.13 might not hold. The expression at 77.13 might not evaluate to true.

+  76.3: Method might lock/unlock more than allowed.

+  191.5: The precondition at 182.14 might not hold. Insufficient epsilons at 182.14  for ReadSharing.x.

+  202.3: The postcondition at 204.13 might not hold. Insufficient epsilons at 204.13  for ReadSharing.x.

+

+Boogie program verifier finished with 51 verified, 4 errors

+------ Running regression test prog4.chalice 

+  5.5: Assertion might not hold. The expression at 5.12 might not evaluate to true.

+  15.7: The held field of the target of the release statement might not be writable.

+  27.7: The held field of the target of the release statement might not be writable.

+

+Boogie program verifier finished with 6 verified, 3 errors

+------ Running regression test RockBand.chalice 

+  27.3: The postcondition at 29.13 might not hold. Insufficient fraction at 29.13 for RockBand.Valid.

+  41.10: Location might not be readable.

+  50.5: Location might not be writable

+  58.3: The postcondition at 60.13 might not hold. Insufficient fraction at 60.13 for Guitar.Valid.

+  77.3: The postcondition at 79.13 might not hold. Insufficient fraction at 79.13 for Vocalist.Valid.

+  96.3: The postcondition at 98.13 might not hold. Insufficient fraction at 98.13 for Organ.Valid.

+

+Boogie program verifier finished with 29 verified, 6 errors

+------ Running regression test swap.chalice 

+

+Boogie program verifier finished with 5 verified, 0 errors

+------ Running regression test GhostConst.chalice 

+The program did not typecheck.

+7.27: undeclared member c in class C

+13.10: ghost variable not allowed here

+21.10: ghost variable not allowed here

+29.10: ghost fields not allowed here

+------ Running regression test OwickiGries.chalice 

+

+Boogie program verifier finished with 5 verified, 0 errors

+------ Running regression test cell-defaults.chalice 

+  96.5: The heap of the callee might not be strictly smaller than the heap of the caller.

+  102.5: The heap of the callee might not be strictly smaller than the heap of the caller.

+  131.5: Assertion might not hold. Automatic fold might fail. Insufficient fraction at 42.5 for Cell.x.

+

+Boogie program verifier finished with 29 verified, 3 errors

+------ Running regression test RockBand-automagic.chalice 

+

+Boogie program verifier finished with 35 verified, 0 errors

+------ Running regression test Leaks.chalice 

+  6.3: Monitor invariant is not allowed to hold write permission to this.mu

+  11.3: Monitor invariant can hold permission of other o.mu field only this.mu if this.mu<<o.mu

+  16.3: Monitor invariant can hold permission of other o.mu field only this.mu if this.mu<<o.mu

+  29.3: Monitor invariant can hold permission of other o.mu field only this.mu if this.mu<<o.mu

+  62.3: Monitor invariant is not allowed to hold write permission to this.mu

+

+Boogie program verifier finished with 7 verified, 5 errors

diff --git a/Chalice/examples/AssociationList.chalice b/Chalice/examples/AssociationList.chalice
new file mode 100644
index 00000000..6adcbef5
--- /dev/null
+++ b/Chalice/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) && maxlock << this

+  {

+    head := new Node

+    head.next := null

+    share head

+    share this between maxlock and head

+  }

+

+  method Add(key: int, value: Data)

+    requires value != null

+    requires rd(mu) && maxlock << 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) && maxlock << 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) && maxlock == p.next.mu

+          invariant p.next.next != null ==> maxlock << 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

+}

diff --git a/Chalice/examples/ForkJoin.chalice b/Chalice/examples/ForkJoin.chalice
new file mode 100644
index 00000000..e79cded9
--- /dev/null
+++ b/Chalice/examples/ForkJoin.chalice
@@ -0,0 +1,77 @@
+/* Example taken from ESOP submission */

+

+class T {

+  var k: int;

+  var l: int;

+

+  method run()

+    requires acc(k);

+    ensures acc(k) && k == old(k) + 1;

+  {

+    k := k + 1;

+  }

+}

+

+class Program {

+  method main() {

+    var x := new T;

+    x.k := 17;

+    x.l := 20;

+    fork tok := x.run();

+    x.l := 10;

+    join tok;

+    assert x.k == 18 && x.l == 10;

+  }

+

+  method justJoin(tok: token<T.run>, x: T) returns (rt: int) 

+    requires x!=null && tok!=null && acc(tok.joinable) && tok.joinable && eval(tok.fork x.run(), acc(x.k));

+    ensures rt == old(eval(tok.fork x.run(), x.k)) + 1;

+  {

+    join tok;

+    rt := x.k;

+  }

+}

+

+/* example using asynchronous method calls */

+

+class C {

+  var x: int;

+

+  method m(v: int) returns (rt: int)

+    ensures rt == v + 1;

+  {

+    rt := v + 1;

+  }

+}

+

+class Program2 {

+  method main1(){

+    var c := new C;

+    var tok: token<C.m>;

+    fork tok := c.m(5);

+

+    // do some computation

+    

+    var x : int;

+    join x := tok;

+    assert x == 6;

+  }

+

+  method main2(){

+    var c := new C;

+    var tok: token<C.m>;

+    fork tok := c.m(5);

+

+    // do some computation

+    

+    call foo(tok, c);

+  }

+

+  method foo(tok: token<C.m>, o: C)

+    requires tok!=null && acc(tok.joinable) && tok.joinable && eval(tok.fork o.m(5), true);

+  {

+    var x: int;

+    join x := tok;

+    assert x == 6;

+  }

+}
\ No newline at end of file
diff --git a/Chalice/examples/HandOverHand.chalice b/Chalice/examples/HandOverHand.chalice
new file mode 100644
index 00000000..f0f6323a
--- /dev/null
+++ b/Chalice/examples/HandOverHand.chalice
@@ -0,0 +1,130 @@
+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,*) && maxlock << 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 maxlock and t

+  }

+

+  method Insert(x: int)

+    requires rd(mu) && maxlock << this

+    requires acc(sum,80) && 0 <= x

+    ensures rd(mu)

+    ensures acc(sum,80) && sum == old(sum) + x

+  {

+    acquire this

+    assert maxlock == 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) && rd(p.val) && acc(p.mu,50)

+      invariant holds(p) && maxlock == p.mu

+      invariant p.next != null ==> acc(p.next.mu,50) && p << p.next

+      invariant p.next != null ==> rd(p.next.val) && 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) && maxlock << 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) && rd(p.val) && acc(p.mu,50)

+      invariant holds(p) && maxlock == p.mu && !assigned(c)

+      invariant p.next != null ==> acc(p.next.mu,50) && p << p.next

+      invariant p.next != null ==> rd(p.next.val) && 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)

+}

diff --git a/Chalice/examples/OwickiGries.chalice b/Chalice/examples/OwickiGries.chalice
new file mode 100644
index 00000000..63f029e8
--- /dev/null
+++ b/Chalice/examples/OwickiGries.chalice
@@ -0,0 +1,35 @@
+class OwickiGries {

+  var counter: int

+  ghost var c0: int

+  ghost var c1: int

+  invariant acc(counter) && acc(c0,50) && acc(c1,50) && counter == c0 + c1

+

+  method Main() {

+    var og := new OwickiGries{ counter := 0, c0 := 0, c1 := 0 }

+    share og

+

+    fork tk0 := og.Worker(false)

+    fork tk1 := og.Worker(true)

+    join tk0; join tk1

+

+    acquire og; unshare og

+    assert og.counter == 2

+  }

+

+  method Worker(b: bool)

+    requires rd(mu) && maxlock << mu

+    requires (!b ==> acc(c0,50)) && (b ==> acc(c1,50))

+    ensures rd(mu)

+    ensures !b ==> acc(c0,50) && c0 == old(c0) + 1

+    ensures b ==> acc(c1,50) && c1 == old(c1) + 1

+  {

+    lock (this) {

+      counter := counter + 1

+      if (!b) {

+        c0 := c0 + 1

+      } else {

+        c1 := c1 + 1

+      }

+    }

+  }

+}

diff --git a/Chalice/examples/RockBand-automagic.chalice b/Chalice/examples/RockBand-automagic.chalice
new file mode 100644
index 00000000..d231ae5a
--- /dev/null
+++ b/Chalice/examples/RockBand-automagic.chalice
@@ -0,0 +1,111 @@
+// verify this program with -checkLeaks -defaults -autoFold -autoMagic

+

+class Client {

+  method Main() {

+    var b := new RockBand

+    call b.Init()

+    call b.Play()

+    call b.Play()

+    call b.Dispose()

+  }

+}

+

+class RockBand module M {

+  var gigs: int

+  var gt: Guitar

+  var doowops: seq<Vocalist>

+  var b3: Organ

+  predicate Valid {

+    /*acc(gigs) &&*/ 0 <= gigs &&

+    /*acc(gt) && gt != null &&*/ gt.Valid &&

+    acc(gt.mu) &&

+    acc(doowops) &&

+    /*acc(b3) && b3 != null &&*/ b3.Valid &&

+    acc(b3.mu)

+  }

+

+  method Init()

+    requires acc(this.*)

+    ensures Valid

+  {

+    gigs := 0

+    gt := new Guitar

+    call gt.Init()

+    b3 := new Organ

+    call b3.Init()

+  }

+

+  method Dispose()

+    requires Valid && acc(mu)

+  {

+    call gt.Dispose()

+    call b3.Dispose()

+    free this

+  }

+

+  method Play()

+    requires Valid

+    ensures Valid

+  {

+    gigs := gigs + 1

+    call gt.Strum()

+    call b3.Grind()

+  }

+}

+

+class Guitar module Musicians {

+  predicate Valid { true }

+  method Init()

+    requires acc(this.*)

+    ensures Valid

+  {

+  }

+  method Dispose()

+    requires Valid && acc(mu)

+  {

+    free this

+  }

+  method Strum()

+    requires Valid

+    ensures Valid

+  {

+  }

+}

+

+class Vocalist module Musicians {

+  predicate Valid { true }

+  method Init()

+    requires acc(this.*)

+    ensures Valid

+  {

+  }

+  method Dispose()

+    requires Valid && acc(mu)

+  {

+    free this

+  }

+  method Strum()

+    requires Valid

+    ensures Valid

+  {

+  }

+}

+

+class Organ module Musicians {

+  predicate Valid { true }

+  method Init()

+    requires acc(this.*)

+    ensures Valid

+  {

+  }

+  method Dispose()

+    requires Valid && acc(mu)

+  {

+    free this

+  }

+  method Grind()

+    requires Valid

+    ensures Valid

+  {

+  }

+}

diff --git a/Chalice/examples/RockBand.chalice b/Chalice/examples/RockBand.chalice
new file mode 100644
index 00000000..c7a2bba0
--- /dev/null
+++ b/Chalice/examples/RockBand.chalice
@@ -0,0 +1,111 @@
+// verify this program with -checkLeaks -defaults -autoFold

+

+class Client {

+  method Main() {

+    var b := new RockBand

+    call b.Init()

+    call b.Play()

+    call b.Play()

+    call b.Dispose()

+  }

+}

+

+class RockBand module M {

+  var gigs: int

+  var gt: Guitar

+  var doowops: seq<Vocalist>

+  var b3: Organ

+  predicate Valid {

+    acc(gigs) && 0 <= gigs &&

+    acc(gt) && gt != null && gt.Valid &&

+    acc(gt.mu) &&  // to enable an eventual free

+    acc(doowops) && //forall{d: Vocalist in doowops; d != null && d.Valid} &&

+    acc(b3) && b3 != null && b3.Valid &&

+    acc(b3.mu)  // to enable an eventual free

+  }

+

+  method Init()

+    requires acc(this.*)

+    ensures Valid

+  {

+    gigs := 0

+    gt := new Guitar

+    call gt.Init()

+    b3 := new Organ

+    call b3.Init()

+  }

+

+  method Dispose()

+    requires Valid && acc(mu)

+  {

+    call gt.Dispose()

+    call b3.Dispose()

+    free this

+  }

+

+  method Play()

+    requires Valid

+    ensures Valid

+  {

+    gigs := gigs + 1

+    call gt.Strum()

+    call b3.Grind()

+  }

+}

+

+class Guitar module Musicians {

+  predicate Valid { true }

+  method Init()

+    requires acc(this.*)

+    ensures Valid

+  {

+  }

+  method Dispose()

+    requires Valid && acc(mu)

+  {

+    free this

+  }

+  method Strum()

+    requires Valid

+    ensures Valid

+  {

+  }

+}

+

+class Vocalist module Musicians {

+  predicate Valid { true }

+  method Init()

+    requires acc(this.*)

+    ensures Valid

+  {

+  }

+  method Dispose()

+    requires Valid && acc(mu)

+  {

+    free this

+  }

+  method Strum()

+    requires Valid

+    ensures Valid

+  {

+  }

+}

+

+class Organ module Musicians {

+  predicate Valid { true }

+  method Init()

+    requires acc(this.*)

+    ensures Valid

+  {

+  }

+  method Dispose()

+    requires Valid && acc(mu)

+  {

+    free this

+  }

+  method Grind()

+    requires Valid

+    ensures Valid

+  {

+  }

+}

diff --git a/Chalice/examples/cell-defaults.chalice b/Chalice/examples/cell-defaults.chalice
new file mode 100644
index 00000000..4781db97
--- /dev/null
+++ b/Chalice/examples/cell-defaults.chalice
@@ -0,0 +1,152 @@
+// verify this program with -defaults -autoFold -autoMagic

+

+class Cell module Library {

+  var x: int;

+

+  method init(v: int)

+    requires acc(this.x) && 0<=v;

+    ensures valid && this.get() == v;

+  {

+    x := v;

+  }

+

+  method set(v: int)

+    requires valid && 0<=v;

+    ensures valid && get()==v;

+  {

+    x := v;

+  }

+  

+  method increment()

+    requires valid;

+    ensures valid && get() == old(get()) + 1;

+  {

+    x := x + 1;

+  }

+

+  method dispose()

+    requires valid && acc(mu);

+    ensures true;

+  {

+    free this;

+  }

+

+  function get(): int

+    requires valid;

+    ensures 0<=result;

+  {

+    x

+  }

+

+  predicate valid {

+    acc(this.x) && 0<=x

+  }

+

+  invariant valid;

+}

+

+class Interval module Library2 {

+  var left: Cell;

+  var right: Cell;

+

+  method init(l: int, r: int)

+    requires 0<=l && l <= r;

+    requires acc(left) && acc(right);

+    ensures valid;

+    ensures getLeft()==l

+    ensures getRight()==r;

+  {

+    left := new Cell;

+    call left.init(l);

+    right := new Cell;

+    call right.init(r);

+  }

+

+  method setLeft(l: int)

+    requires valid;

+    requires 0<=l && l<=getRight();

+    ensures valid;

+    ensures getLeft()==l && getRight()==old(getRight());

+  {

+    call left.set(l);

+  }

+

+  method setRight(r: int)

+    requires valid;

+    requires 0<=r && getLeft()<=r;

+    ensures valid;

+    ensures getLeft()==old(getLeft()) && getRight()==r;

+  {

+    call right.set(r);

+  }

+

+  method shift(v: int)

+    requires valid;

+    requires 0<=v;

+    ensures valid;

+    ensures getLeft()==old(getLeft())+v && getRight()==old(getRight())+v;

+  {

+    call left.set(left.get()+v);

+    call right.set(right.get()+v);

+  }

+

+  function getLeft() : int

+    requires valid;

+  {

+    left.get() // for some reason, Boogie can't figure out the callee's heap is smaller when using defaults

+  }

+

+  function getRight() : int

+    requires valid;

+  {

+    right.get() // for some reason, Boogie can't figure out the callee's heap is smaller when using defaults

+  }

+  

+  predicate valid

+  {

+    left.valid && right.valid && left.get() <= right.get()

+  }

+}

+

+class Program module Main {

+  method main(){

+    var c1 := new Cell;

+    call c1.init(5);

+    call c1.set(6);

+

+    var c2 := new Cell;

+    call c2.init(10);

+    call c2.set(11);

+

+    assert c1.get() == 6;

+  }

+

+  method main2(){

+    var c: Cell;

+

+    c := new Cell;

+    call c.init(0);

+    call c.dispose();

+

+    assert c.valid; // should fail

+  }

+

+  method main3() returns (rt: Cell)

+    ensures rt!=null && rt.valid && rt.get() == 0

+  {

+    rt := new Cell;

+    call rt.init(0)

+  }

+

+  method main4() {

+    var c: Cell;

+

+    c := new Cell;

+    call c.init(0);

+    share c;

+

+    acquire c;

+    call c.set(1);

+    release c;

+  }

+}
\ No newline at end of file
diff --git a/Chalice/examples/cell.chalice b/Chalice/examples/cell.chalice
new file mode 100644
index 00000000..d4003a3c
--- /dev/null
+++ b/Chalice/examples/cell.chalice
@@ -0,0 +1,163 @@
+class Cell module Library {

+  var x: int;

+

+  method init(v: int)

+    requires acc(this.x) && 0<=v;

+    ensures valid && this.get() == v;

+  {

+    x := v;

+    fold valid;

+  }

+

+  method set(v: int)

+    requires valid && 0<=v;

+    ensures valid && get()==v;

+  {

+    unfold valid;

+    x := v;

+    fold valid;

+  }

+  

+  method increment()

+    requires valid;

+    ensures valid && get() == old(get()) + 1;

+  {

+    unfold valid;

+    x := x + 1;

+    fold valid;

+  }

+

+  method dispose()

+    requires valid && acc(mu);

+    ensures true;

+  {

+    unfold valid;

+    free this;

+  }

+

+  function get(): int

+    requires valid;

+    ensures 0<=result;

+  {

+    unfolding valid in x

+  }

+

+  predicate valid {

+    acc(this.x) && 0<=x

+  }

+

+  invariant valid;

+}

+

+class Interval module Library2 {

+  var left: Cell;

+  var right: Cell;

+

+  method init(l: int, r: int)

+    requires 0<=l && l <= r;

+    requires acc(left) && acc(right);

+    ensures valid;

+    ensures getLeft()==l

+    ensures getRight()==r;

+  {

+    left := new Cell;

+    call left.init(l);

+    right := new Cell;

+    call right.init(r);

+    fold valid;

+  }

+

+  method setLeft(l: int)

+    requires valid;

+    requires 0<=l && l<=getRight();

+    ensures valid;

+    ensures getLeft()==l && getRight()==old(getRight());

+  {

+    unfold valid;

+    call left.set(l);

+    fold valid;

+  }

+

+  method setRight(r: int)

+    requires valid;

+    requires 0<=r && getLeft()<=r;

+    ensures valid;

+    ensures getLeft()==old(getLeft()) && getRight()==r;

+  {

+    unfold valid;

+    call right.set(r);

+    fold valid;

+  }

+

+  method shift(v: int)

+    requires valid;

+    requires 0<=v;

+    ensures valid;

+    ensures getLeft()==old(getLeft())+v && getRight()==old(getRight())+v;

+  {

+    unfold valid;

+    call left.set(left.get()+v);

+    call right.set(right.get()+v);

+    fold valid;

+  }

+

+  function getLeft() : int

+    requires valid;

+  {

+    unfolding valid in left.get()

+  }

+

+  function getRight() : int

+    requires valid;

+  {

+    unfolding valid in right.get()

+  }

+  

+  predicate valid

+  {

+    acc(left) && acc(right) && left!=null && right!=null && left.valid && right.valid && left.get() <= right.get()

+  }

+}

+

+class Program module Main {

+  method main(){

+    var c1 := new Cell;

+    call c1.init(5);

+    call c1.set(6);

+

+    var c2 := new Cell;

+    call c2.init(10);

+    call c2.set(11);

+

+    assert c1.get() == 6;

+  }

+

+  method main2(){

+    var c: Cell;

+

+    c := new Cell;

+    call c.init(0);

+    call c.dispose();

+

+    assert c.valid; // should fail

+  }

+

+  method main3() returns (rt: Cell)

+    ensures rt!=null && rt.valid && rt.get() == 0

+  {

+    rt := new Cell;

+    call rt.init(0)

+  }

+

+  method main4() {

+    var c: Cell;

+

+    c := new Cell;

+    call c.init(0);

+    share c;

+

+    acquire c;

+    call c.set(1);

+    release c;

+  }

+}
\ No newline at end of file
diff --git a/Chalice/examples/counter.chalice b/Chalice/examples/counter.chalice
new file mode 100644
index 00000000..0cab7736
--- /dev/null
+++ b/Chalice/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) && maxlock << 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) && maxlock << 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) && maxlock << c.mu;

+  {

+    lock (c) {

+      release c

+      acquire c

+    }

+  }

+

+  method nestedGood1(c: Counter)

+    requires c != null && acc(c.mu) && maxlock << 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) && maxlock << c.mu;

+  {

+    lock (c) {

+      release c

+    }  // error: no longer holds c

+  }

+

+  method nestedBad1(c: Counter)

+    requires c != null && acc(c.mu) && maxlock << c.mu;

+  {

+    lock (c) {

+      acquire c  // error: already holds c

+    }

+  }

+

+  method nestedBad2(c: Counter)

+    requires c != null && acc(c.mu) && maxlock << c.mu;

+  {

+    lock (c) {

+      lock (c) {  // error: already holds c

+      }

+    }

+  }

+

+  method nestedBad3(c: Counter)

+    requires c != null && acc(c.mu) && maxlock << 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
diff --git a/Chalice/examples/dining-philosophers.chalice b/Chalice/examples/dining-philosophers.chalice
new file mode 100644
index 00000000..6a67174c
--- /dev/null
+++ b/Chalice/examples/dining-philosophers.chalice
@@ -0,0 +1,93 @@
+class Philosopher module Philosophers {

+  var left: Fork;

+  var right: Fork;

+  

+  method init(f1: Fork, f2: Fork) 

+    requires f1!=null && f2!=null;

+    requires acc(this.*);

+    ensures valid;

+    ensures getLeft()==f1 && getRight()==f2;

+  {

+    left := f1;

+    right := f2;

+    fold valid;

+  }

+

+  method run()

+    requires valid;

+    requires acc(getLeft().mu, 10);

+    requires acc(getRight().mu, 10);

+    requires maxlock << getLeft().mu;

+    requires maxlock << getRight().mu;

+    requires getLeft().mu << getRight().mu;

+  {

+    while(true)

+      invariant valid && acc(getLeft().mu, 10) && acc(getRight().mu, 10) && maxlock << getLeft().mu && maxlock << getRight().mu && getLeft().mu << getRight().mu;

+    {

+      unfold valid;

+      acquire left;

+      acquire right;

+      //eat

+      release left;

+      release right;

+      fold valid;

+    }

+  }

+

+  function getLeft(): Fork 

+    requires valid;

+    ensures result!=null;

+  {

+    unfolding valid in left

+  }

+

+  function getRight(): Fork 

+    requires valid;

+    ensures result!=null;

+  {

+    unfolding valid in right

+  }

+

+  predicate valid {

+    acc(left) && acc(right) && left!=null && right!=null

+  }

+}

+

+class Fork module Dining {

+  invariant true;

+}

+

+class Program module Main {

+  method main(){

+    // create forks

+    var f1 := new Fork;

+    var f2 := new Fork;

+    var f3 := new Fork;

+

+    share f1;

+    share f2 above f1;

+    share f3 above f1, f2;

+

+    // create philosophers

+    var aristotle := new Philosopher;

+    call aristotle.init(f1, f2);

+

+    var plato := new Philosopher;

+    call plato.init(f2, f3);

+

+    var kant := new Philosopher;

+    call kant.init(f1, f3);

+    

+    assert f2.mu << f3.mu;

+

+    // start eating

+    fork tk0 := aristotle.run();

+    fork tk1 := plato.run();

+    fork tk2 := kant.run();

+

+    // everyone's done

+    join tk0;

+    join tk1;

+    join tk2;

+  }

+}
\ No newline at end of file
diff --git a/Chalice/examples/iterator.chalice b/Chalice/examples/iterator.chalice
new file mode 100644
index 00000000..356e6d83
--- /dev/null
+++ b/Chalice/examples/iterator.chalice
@@ -0,0 +1,150 @@
+class List module Collections {

+  var contents: seq<int>;

+

+  method init()

+    requires acc(contents);

+    ensures valid && size(100)==0;

+  {

+    contents := nil<int>;

+    fold valid; 

+  }

+

+  method add(x: int) 

+    requires valid;

+    ensures valid && size(100) == old(size(100)+1) && get(size(100)-1, 100) == x;

+    ensures forall { i in [0:size(100)-1]; get(i, 100) == old(get(i, 100)) };

+  {

+    unfold valid;

+    contents := contents ++ [x];

+    fold valid;

+  }

+

+  function get(index: int, f: int): int 

+    requires 0<f && f<=100 && acc(valid, f) && (0<=index && index<size(f));

+    ensures forall { i in [1:f]; get(index, f) == get(index, i)};

+  {

+    unfolding acc(valid, f) in contents[index]

+  }

+

+  function size(f: int): int 

+    requires 0<f && f<=100 && acc(valid, f);

+    ensures 0<=result;

+    ensures forall { i in [1:f]; size(f) == size(i)};

+  {

+    unfolding acc(valid, f) in |contents|

+  }

+

+  predicate valid {

+    acc(contents)

+  }

+}

+

+class Iterator module Collections {

+  var list: List;

+  var index: int;

+  var frac: int;

+

+  method init(l: List, f: int)

+    requires 0<f && f<=100;

+    requires acc(list) && acc(index) && acc(frac);

+    requires l!=null;

+    requires acc(l.valid, f);

+    ensures valid;

+    ensures getList()==l;

+    ensures getFraction()==f;

+  {

+    list := l;

+    this.index := 0;

+    frac := f;

+    fold valid;

+  }

+

+  method next() returns (rt: int) 

+    requires valid && hasNext();

+    ensures valid;

+    ensures getList()==old(getList());

+    ensures getFraction()==old(getFraction());

+  {

+    unfold valid;

+    rt := list.get(index, frac);

+    index := index + 1;

+    fold valid;

+  }

+

+  method dispose()

+    requires valid;

+    ensures acc(old(getList()).valid, old(getFraction()));

+  {

+    unfold valid;

+  }

+

+  function hasNext(): bool 

+    requires valid;

+  {

+    unfolding valid in index<list.size(frac)

+  }

+

+  function getFraction(): int

+    requires valid;

+    ensures 0<result && result<=100;

+  {

+    unfolding valid in frac

+  }

+

+  function getList(): List

+    requires valid;

+    ensures getList()!=null;

+  {

+    unfolding valid in list

+  }

+

+  predicate valid

+  {

+    acc(list) && acc(index) && acc(frac) && 0<frac && frac<=100 && list!=null && acc(list.valid, frac) && 0<=index && index<=list.size(frac)

+  }

+}

+

+class Program module Main {

+  method main(){

+    var tmp: int;

+    //create a new list

+    var list := new List;

+    call list.init();

+    call list.add(5);

+    call list.add(6);

+ 

+    // create a new iterator

+    var iter1 := new Iterator;

+    assert list!=null; // needed here: triggering problem?

+    assert list.size(100)==2;

+    assert list.size(50)==2;

+    call iter1.init(list, 10);

+

+    // create a second iterator

+    var iter2 := new Iterator;

+    assert list!=null; // needed here: triggering problem?

+    call iter2.init(list, 10);

+    

+    // iterate over the list

+    while(iter1.hasNext())

+      invariant iter1.valid && iter1.getList()==list && iter1.getFraction()==10;

+    {

+      call tmp := iter1.next();

+    }

+

+    // iterate over the list

+    while(iter2.hasNext())

+      invariant iter2.valid && iter2.getList()==list && iter2.getFraction()==10;

+    {

+      call tmp := iter2.next();

+    }

+

+    // dispose the iterators

+    call iter1.dispose();

+    call iter2.dispose();

+

+    // full access to the list

+    assert list.valid;

+    assert list.size(50)==2;

+  }

+}
\ No newline at end of file
diff --git a/Chalice/examples/iterator2.chalice b/Chalice/examples/iterator2.chalice
new file mode 100644
index 00000000..5b75c1ca
--- /dev/null
+++ b/Chalice/examples/iterator2.chalice
@@ -0,0 +1,134 @@
+/* Iterator pattern in Chalice. */

+

+class List module Collections {

+  var contents: seq<int>;

+

+  method init()

+    requires acc(contents);

+    ensures valid && size()==0;

+  {

+    contents := nil<int>;

+    fold valid; 

+  }

+

+  method add(x: int) 

+    requires valid;

+    ensures valid && size() == old(size()+1) && get(size()-1) == x; // I don't know why this happens.

+    ensures forall { i in [0:size()-1]; get(i) == old(get(i)) };

+  {

+    unfold valid;

+    contents := contents ++ [x];

+    fold valid;

+  }

+

+  function get(index: int): int 

+    requires rd(valid) && 0<=index && index<size();

+  {

+    unfolding rd(valid) in contents[index]

+  }

+

+  function size(): int 

+    requires rd(valid);

+    ensures 0<=result;

+  {

+    unfolding rd(valid) in |contents|

+  }

+

+  predicate valid {

+    acc(contents)

+  }

+}

+

+class Iterator module Collections {

+  var list: List;

+  var index: int;

+

+  method init(l: List)

+    requires acc(list) && acc(index);

+    requires l!=null;

+    requires rd(l.valid);

+    ensures valid;

+    ensures getList()==l;

+  {

+    list := l;

+    this.index := 0;

+    fold valid;

+  }

+

+  method next() returns (rt: int) 

+    requires valid && hasNext();

+    ensures valid;

+    ensures getList()==old(getList());

+  {

+    unfold valid;

+    rt := list.get(index);

+    index := index + 1;

+    fold valid;

+  }

+

+  method dispose()

+    requires valid;

+    ensures rd(old(getList()).valid);

+  {

+    unfold valid;

+  }

+

+  function hasNext(): bool 

+    requires valid;

+  {

+    unfolding valid in index<list.size()

+  }

+

+  function getList(): List

+    requires valid;

+    ensures result!=null;

+  {

+    unfolding valid in list

+  }

+

+  predicate valid

+  {

+    acc(list) && acc(index) && list!=null && rd(list.valid) && 0<=index && index<=list.size()

+  }

+}

+

+class Program module Main {

+  method main(){

+    var tmp: int;

+    //create a new list

+    var list := new List;

+    call list.init();

+    call list.add(5);

+    call list.add(6);

+ 

+    // create a new iterator

+    var iter1 := new Iterator;

+    call iter1.init(list);

+

+    // create a second iterator

+    var iter2 := new Iterator;

+    call iter2.init(list);

+    

+    // iterate over the list

+    while(iter1.hasNext())

+      invariant iter1.valid && iter1.getList()==list;

+    {

+      call tmp := iter1.next();

+    }

+

+    // iterate over the list

+    while(iter2.hasNext())

+      invariant iter2.valid && iter2.getList()==list;

+    {

+      call tmp := iter2.next();

+    }

+

+    // dispose the iterators

+    call iter1.dispose();

+    call iter2.dispose();

+

+    // full access to the list

+    assert list.valid;

+    assert list.size()==2;

+  }

+}
\ No newline at end of file
diff --git a/Chalice/examples/linkedlist.chalice b/Chalice/examples/linkedlist.chalice
new file mode 100644
index 00000000..acde86ab
--- /dev/null
+++ b/Chalice/examples/linkedlist.chalice
@@ -0,0 +1,61 @@
+/* Recursive implementation and specification of a linked list. */

+

+class Node {

+  var next: Node;

+  var value: int;

+

+  method init(v: int)

+    requires acc(next) && acc(value);

+    ensures valid && size() == 1;

+  {

+    next := null;

+    value := v;

+    fold this.valid;

+  }

+

+  method add(x: int) 

+    requires valid;

+    ensures valid;

+    ensures size() == old(size())+1;

+  {

+    unfold this.valid;

+    if(next==null) {

+      var n : Node;

+      n := new Node;

+      call n.init(x);

+      next := n;

+    } else {

+      call next.add(x);

+    }

+    fold this.valid;

+  }

+

+  method addFirst(x: int) returns (rt: Node)

+    requires valid;

+    ensures rt!=null && rt.valid;

+    ensures rt.size() == old(size()) + 1;

+  {

+    var n: Node;

+    n := new Node;

+    n.value := x;

+    n.next := this; 

+    fold n.valid;

+    rt := n;

+  }

+

+  function at(i: int): int

+    requires valid && 0<=i && i<size();

+  {

+    unfolding valid in i==0 ? value : next.at(i-1)  // no warning anymore... fishy!

+  }

+

+  function size(): int

+    requires valid;

+  {

+    unfolding this.valid in (next!=null ? 1+ next.size() : 1)

+  }

+

+  predicate valid {

+    acc(next) && acc(value) && (next!=null ==> next.valid)

+  }

+}
\ No newline at end of file
diff --git a/Chalice/examples/producer-consumer.chalice b/Chalice/examples/producer-consumer.chalice
new file mode 100644
index 00000000..f2c751d9
--- /dev/null
+++ b/Chalice/examples/producer-consumer.chalice
@@ -0,0 +1,202 @@
+class Program {

+  method main(){

+    var buffer := new Queue;

+    call buffer.init();

+    share buffer;

+

+    var producer := new Producer;

+    call producer.init(buffer);

+    fork tkP := producer.run();

+

+    var consumer := new Consumer;

+    call consumer.init(buffer);

+    fork tkC := consumer.run();

+

+    join tkP;

+    join tkC;

+  

+    acquire buffer;

+    unshare buffer;

+

+    var tmp := buffer.size();

+  }

+}

+

+class Producer module Producer {

+  var buffer: Queue;

+

+  method init(buff: Queue)

+    requires acc(buffer) && buff!=null;

+    ensures valid && getBuffer()==buff;

+  {

+    buffer := buff;

+    fold valid;

+  }

+

+  method run()

+    requires valid && rd(getBuffer().mu) && maxlock << getBuffer().mu;

+    ensures rd(old(getBuffer()).mu);

+  {

+    var tmp: int;

+

+    while(true)

+      invariant valid && rd(getBuffer().mu) && maxlock << getBuffer().mu;

+    {

+      unfold valid;

+      acquire buffer;

+      call buffer.enqueue(5);

+      release buffer;

+      fold valid;

+    }

+    unfold valid;

+  }

+

+  function getBuffer(): Queue

+    requires valid;

+    ensures result!=null;

+  {

+    unfolding valid in buffer

+  }

+

+  predicate valid {

+    acc(buffer) && buffer!=null

+  }

+}

+

+class Consumer module Consumer {

+  var buffer: Queue;

+

+  method init(buff: Queue)

+    requires acc(buffer) && buff!=null;

+    ensures valid && getBuffer()==buff;

+  {

+    buffer := buff;

+    fold valid;

+  }

+

+  method run()

+    requires valid && rd(getBuffer().mu) && maxlock << getBuffer().mu;

+    ensures rd(old(getBuffer()).mu);

+  {

+    while(true)

+      invariant valid && rd(getBuffer().mu) && maxlock << getBuffer().mu;

+    {

+      unfold valid;

+      acquire buffer;

+      if(0<=buffer.size()){

+        call buffer.enqueue(5);

+      }

+      release buffer;

+      fold valid;

+    }

+    unfold valid;

+  }

+

+  function getBuffer(): Queue

+    requires valid;

+    ensures result!=null;

+  {

+    unfolding valid in buffer

+  }

+

+  predicate valid {

+    acc(buffer) && buffer!=null

+  }

+}

+

+class Queue module Queue {

+  var contents: List;

+

+  invariant valid;

+

+  method init()

+    requires acc(contents);

+    ensures valid;

+    ensures size()==0;

+  {

+    contents := new List;

+    call contents.init();

+    fold valid;

+  }

+

+  method enqueue(x: int) 

+    requires valid;

+    ensures valid;

+    ensures size() == old(size())+1;

+  {

+    unfold valid;

+    call contents.add(x);

+    fold valid;

+  }

+

+  method dequeue() returns (rt: int)

+    requires valid && 0<size();

+    ensures valid;

+    ensures size() == old(size())-1;

+  {

+    unfold valid;

+    call rt := contents.removeFirst();

+    fold valid;

+  }

+

+  function size(): int

+    requires valid;

+  {

+    unfolding valid in contents.size()

+  }

+

+  predicate valid {

+    acc(contents) && contents!=null && contents.valid

+  }

+}

+

+class List module Collections {

+  var contents: seq<int>;

+

+  method init()

+    requires acc(contents);

+    ensures valid && size()==0;

+  {

+    contents := nil<int>;

+    fold valid; 

+  }

+

+  method add(x: int) 

+    requires valid;

+    ensures valid && size() == old(size()+1) && get(size()-1) == x;

+    ensures forall { i in [0:size()-1]; get(i) == old(get(i)) };

+  {

+    unfold valid;

+    contents := contents ++ [x];

+    fold valid;

+  }

+

+  method removeFirst() returns (rt: int) 

+    requires valid && 0<size();

+    ensures valid && size() == old(size()-1);

+    ensures forall { i  in [0:size()]; get(i) == old(get(i+1)) };

+  {

+    unfold valid;

+    rt := contents[0];

+    contents := contents[1..];

+    fold valid;

+  }

+

+

+  function get(index: int): int 

+    requires rd(valid) && 0<=index && index<size();

+  {

+    unfolding rd(valid) in contents[index]

+  }

+

+  function size(): int 

+    requires rd(valid);

+    ensures 0<=result;

+  {

+    unfolding rd(valid) in |contents|

+  }

+

+  predicate valid {

+    acc(contents)

+  }

+}
\ No newline at end of file
diff --git a/Chalice/examples/prog0.chalice b/Chalice/examples/prog0.chalice
new file mode 100644
index 00000000..da351c85
--- /dev/null
+++ b/Chalice/examples/prog0.chalice
@@ -0,0 +1,65 @@
+class C {

+  method m() {

+    assert 4 + (a * 5) + (2 + 3) * (a + a);

+    a := a + 3;

+    b := a - b - c + 4 * d + 20 + --25;

+    b := ((((a - b) - c) + 4 * d) + 20) + --25;

+    c := a - (b - (c + (4 * d + (20 + 25))));

+    assert (X ==> Y) ==> Z <==> A ==> B ==> C;

+    assume A && B && (C || D || E) && F;

+    var x;

+    var y := 12 + !(x.f.g).h - (!x).f + (!x.f);

+    var z := new C;

+    y := new D;

+    o.f := 5;

+    (a + b).y := new T;

+    reorder (2 ==(O != 3)) != O between a,b,c and x,y,z;

+    reorder X ==> Y below x+5;

+    reorder o.f above this, null;

+    share o;

+    unshare o;

+    acquire o;

+    release o;

+    rd acquire o;

+    rd release o;

+    downgrade o;

+    var tok: token<C.m>;

+    fork tok := o.m();

+    join tok;

+    assert rd(x) + acc(y) + acc(z, 1/4) + old(old(k)) + null.f;

+    x := this.f;

+    call m(2,3,4);

+    call this.m(2,3,4);

+    call a,b,c := o.m();

+    call x := m(200);

+    reorder o above maxlock;

+  }

+  method p(a,b,c) returns (x,y,z)

+    requires 8 + 2 == 10;

+    ensures 8 + 5 > 10;

+    requires x == y+1;

+    ensures old(x) < x;

+  {

+    if (x == 7) {

+      y := y + 1;  z := z + 2;

+    } else if (x == 8) {

+      y := 2;

+    } else {

+      z := 10;

+    }

+    {  // empty block

+    }

+    if (x == 9) { }

+    if (x == 10) { x := 10; } else { }

+    var n := 0;

+    while (n < 100) { n := n - 1; }

+    while (n != 0)

+      invariant n % 2 == 0;

+      invariant sqrt2 * sqrt2 == 2;

+    {

+      n := n - 2;

+    }

+    call v,x := s.M(65);

+  }

+}

+class D { }

diff --git a/Chalice/examples/prog1.chalice b/Chalice/examples/prog1.chalice
new file mode 100644
index 00000000..133de36d
--- /dev/null
+++ b/Chalice/examples/prog1.chalice
@@ -0,0 +1,86 @@
+// 7 errors expected

+

+class C {

+  var x: int;

+  invariant acc(x) && 0 <= x;

+

+  method seq0() returns (r: int)

+  {

+    r := x;  // error: cannot access this.x here (90)

+  }

+  method seq1() returns (r: int)

+    requires acc(x);

+  {

+    r := x;

+  }

+  method seq2() returns (r: int)

+    requires rd(x);

+  {

+    r := x;

+  }

+  method seq3() returns (r: int)

+    requires rd(x);

+  {

+    r := x;

+    x := x + 1;  // error: cannot write to this.x here (184)

+  }

+

+  method main0()

+  {

+    var c := new C;

+    c.x := 0;

+    share c;

+    var t := c.x;  // error: cannot access c.x now (254)

+  }

+  method main1()

+  {

+    var c := new C;

+    c.x := 2;

+    share c;

+    acquire c;

+    c.x := c.x - 1;

+    release c;  // error: monitor invariant might not hold (362)

+  }

+  method main2()

+  {

+    var c := new C;

+    c.x := 2;

+    share c;

+    acquire c;

+    c.x := c.x + 1;

+    release c;  // good!

+  }

+  method main3()

+  {

+    var c := new C;

+    c.x := 2;

+    share c;

+    rd acquire c;

+    var tmp := c.x + 1;  // fine

+    c.x := tmp;  // error: cannot write to c.x here (582)

+    rd release c;

+  }

+  method main4()

+  {

+    var c := new C;

+    c.x := 2;

+    share c;

+    acquire c;

+    c.x := c.x + 1;

+    unshare c;

+    c.x := c.x + 1;

+  }

+  method main5()

+  {

+    var c := new C;

+    unshare c;  // error: cannot unshare an object that isn't shared (754)

+  }

+  method main6()

+  {

+    var c := new C;

+    c.x := 0;

+    share c;  acquire c;

+    unshare c;

+    unshare c;  // error: cannot unshare an object that isn't shared (862)

+  }

+}
\ No newline at end of file
diff --git a/Chalice/examples/prog2.chalice b/Chalice/examples/prog2.chalice
new file mode 100644
index 00000000..55fe8ff5
--- /dev/null
+++ b/Chalice/examples/prog2.chalice
@@ -0,0 +1,93 @@
+// 4 errors expected

+

+class C {

+  method M(x: int) returns (y: bool)

+    requires 0 <= x;

+    ensures y <==> x == 10;

+  {

+    y := true;

+    if (x != 10) { y := !y; }

+  }

+

+  method Caller0()

+  {

+    var b: bool;

+    call b := M(12);

+    assert !b;

+    call b := M(10);

+    assert b;

+  }

+  method Caller1()

+  {

+    var b: bool;

+    call b := M(11);

+    assert b; // error (258)

+  }

+

+  var F: int;

+

+  method P(n: int)

+    requires acc(F);

+    ensures F == old(F) + n;  // error

+  {

+    F := F + n;

+  }

+  method Caller2()

+    requires acc(F);

+  {

+    var prev := F;

+    call P(2);

+    assert false; // succeeds because postcondition of P is not well-defined (i.e. we do not havoc this.F, so the verifier assumes the value is the same in pre and post) 

+  }

+

+  method Q(n: int)

+    requires acc(F);

+    ensures acc(F) && F == old(F) + n;

+  {

+    F := F + n;

+  }

+  method Caller3()

+    requires acc(F);

+    ensures acc(F);

+  {

+    var prev := F;

+    call Q(2);

+    assert F == prev + 2;

+  }

+}

+

+class Consts {

+  method M0() returns (z: int)

+    ensures z == 5

+  {

+    const a := 5

+    z := a

+  }

+  method M1() {

+    ghost const a

+    a := 5

+  }

+  method M2() {

+    ghost const a

+    a := 5

+    a := 5  // error (569)

+  }

+  method M3(b: bool) {

+    ghost const a

+    if (b) { a := 5 }

+    assert a < 10  // error (611)

+  }

+  method M4(b: bool) {

+    ghost const a

+    if (b) { a := 5 }

+    ghost var x := a

+    if (!b) { a := 7 }

+    assert a < 10

+    assert b ==> x == 5  // cool, huh?

+  }

+  method M5(b: bool) {

+    ghost const a

+    if (b) { a := 5 }

+    assert assigned(a) ==> a == 5

+  }

+}

diff --git a/Chalice/examples/prog3.chalice b/Chalice/examples/prog3.chalice
new file mode 100644
index 00000000..6c323d0e
--- /dev/null
+++ b/Chalice/examples/prog3.chalice
@@ -0,0 +1,247 @@
+// 4 errors expected

+

+class Main {

+  method A() {

+    var d := new Data;

+    call d.Init();

+    share d;

+

+    var t0: T := new T;  t0.d := d;

+    share t0 between maxlock and d

+    var t1: T := new T;  t1.d := d;

+    share t1 between maxlock and d

+    

+    var t0Token: token<T.run>;

+    fork t0Token := t0.run();

+    var t1Token: token<T.run>;

+    fork t1Token := t1.run();

+

+    join t0Token;  acquire t0; unshare t0;

+    join t1Token;  acquire t1; unshare t1;

+

+    acquire d;  unshare d;

+    assert 0 <= d.x && d.x < 100;

+  }

+

+  method B() returns (r: U)

+    lockchange r;

+  {

+    var u := new U;

+    share u;

+

+    var uToken: token<U.run>;

+    fork uToken := u.run();

+

+    acquire u;  // a little unusual to acquire after a fork, but allowed

+    assert maxlock == u.mu;

+

+    var v := new U;

+    share v;  acquire v;  // this line has the effect of increasing maxlock

+

+    assert maxlock == v.mu;

+    assert maxlock != u.mu;

+    assert u << v;

+    assert u << maxlock;

+

+    join uToken;  // material for the smoke check

+    release u;

+    r := v;

+  }

+  

+  method C()

+    ensures maxlock == old(maxlock);

+  {

+    var u := new U;

+    share u;

+    acquire u;

+    release u;

+  }

+

+  method Mx0()

+  {

+  }

+  method Mx1()

+    lockchange this

+  {

+  }

+  method MxCaller0()

+    ensures maxlock == old(maxlock);

+  {

+  }

+  method MxCaller1()

+    ensures maxlock == old(maxlock);

+  {

+    call Mx0();

+  }

+  method MxCaller2()

+    ensures maxlock == old(maxlock); // error

+  {

+    call Mx1();

+  }  // error: missing lockchange

+

+  method D(u: U)

+    requires u != null && rd(u.mu) && maxlock << u;

+    ensures maxlock == old(maxlock);

+  {

+    acquire u;

+    release u;

+  }

+}

+

+class Data {

+  var x: int;

+  invariant acc(x) && 0 <= x && x < 100;

+  method Init()

+    requires acc(x);

+    ensures acc(x) && x == 0;

+  {

+    x := 0;

+  }

+}

+

+class T {

+  var d: Data;

+  invariant rd(d) && d != null && rd(d.mu) && rd(this.mu) && this << d;

+  method run()

+    requires rd(mu) && maxlock << this;

+    ensures rd(mu);

+  {

+    acquire this;

+    acquire d;

+    d.x := d.x + 1;

+    if (d.x == 100) { d.x := 0; }

+    release d;

+    release this;

+  }

+}

+

+class U {

+  method run()

+    requires rd(mu) && maxlock << this;

+    ensures rd(mu);

+  {

+  }

+}

+

+// Tests that use OLD in postcondition of run:

+

+class X {

+  var k: int

+  var l: int

+

+  method inc()

+    requires acc(k)

+    ensures acc(k) && k == old(k) + 1

+  {

+    k := k + 1

+  }

+  method Client0() returns (y: int)

+    ensures y == 8

+  {

+    var x := new X

+    x.k := 17  x.l := 10

+    call x.inc()

+    assert x.k == 18 && x.l == 10

+    y := x.k - x.l

+  }

+

+  method run()

+    requires acc(k) && 0 <= k

+    ensures acc(k) && k == old(k) + 1

+  {

+    k := k + 1

+  }

+

+  method Client1() returns (y: int)

+    ensures y == 8

+  {

+    var x := new X

+    x.k := 17

+    x.l := 20

+    var xToken: token<X.run>;

+    fork xToken := x.run();

+    x.l := 10

+    join xToken

+    assert x.k == 18 && x.l == 10

+    y := x.k - x.l

+  }

+  method Client2(tk: token<X.run>, x: X) returns (z: int)

+    requires x!=null && tk!=null && acc(tk.joinable) && tk.joinable && eval(tk.fork x.run(), acc(x.k) && 0<=x.k); 

+    ensures 1 <= z

+  {

+    join tk

+    z := x.k

+    assert 1<=x.k;

+  }

+}

+

+class ReadSharing {

+  var x: int

+

+  method Consume()

+    requires rd(x)

+  {

+    // skip

+  }

+

+  method Divulge()  // bad

+    requires rd(x)

+  {

+    call Consume()

+    call Consume()  // error: cannot share twice (1773)

+  }

+

+  method Communicates()  // good

+    requires rd(x,3)

+    ensures rd(x,1)

+  {

+    call Consume()

+    call Consume()

+  }

+

+  method Gossips()  // bad

+    requires rd(x,3)

+    ensures rd(x,1)

+  {

+    call Consume()

+    call Consume()

+    call Consume()

+  }  // error: does not live up to postcondition (2015)

+

+  method Shares()  // good

+    requires rd(x,*)

+    ensures rd(x,*)

+  {

+    call Consume()

+    call Consume()

+    call Consume()

+  }

+

+  method TeamPlayer(N: int)  // good

+    requires 0<=N && rd(x,N)

+    ensures rd(x,0)

+  {

+    var n := N

+    while (0 < n)

+      invariant 0<=n && rd(x,n)

+    {

+      n := n - 1

+    }

+  }

+

+  method Unselfish(N: int)  // good

+    requires rd(x,*)

+    ensures rd(x,*)

+  {

+    var n := N

+    if (N == 173) {

+      call Unselfish(200)

+    }

+    while (0 < n)

+      invariant rd(x,*)

+    {

+      call Consume()

+      n := n - 1

+    }

+  }

+}

diff --git a/Chalice/examples/prog4.chalice b/Chalice/examples/prog4.chalice
new file mode 100644
index 00000000..655c5815
--- /dev/null
+++ b/Chalice/examples/prog4.chalice
@@ -0,0 +1,49 @@
+class LoopTargets {

+  method M() returns (y) {

+    y := 0

+    while (y < 100) { y := y + 1 }

+    assert y == 0  // error (139)

+  }

+  method N() returns (t: LoopTargets)

+    lockchange t

+  {

+    t := new LoopTargets

+    share t

+    acquire t

+    var s := true

+    while (s) {

+      release t  // error: loop invariant does not say holds(t) (252)

+      s := false

+    }

+  }

+  method P() {

+    var t := new LoopTargets

+    share t

+    acquire t

+    var s := true

+    while (s)

+      invariant acc(t.mu) && maxlock == t.mu

+    {

+      release t  // error: loop invariant does not say holds(t) (414)

+      acquire t

+      s := false

+    }

+    release t

+  }

+  method Q() {

+    var t := new LoopTargets

+    share t

+    acquire t

+    var s := true

+    while (s)

+      invariant rd(t.mu)

+      invariant holds(t) && maxlock == t.mu

+    {

+      release t

+      acquire t

+      s := false

+    }

+    assert holds(t)  // there we are

+    release t

+  }

+}

diff --git a/Chalice/examples/swap.chalice b/Chalice/examples/swap.chalice
new file mode 100644
index 00000000..46a6a71a
--- /dev/null
+++ b/Chalice/examples/swap.chalice
@@ -0,0 +1,20 @@
+class C {

+  method m(a, b) returns (x, y)

+    ensures x == a && y == b;

+  {

+    x := a;

+    y := b;

+  }

+

+  var F;

+  var G;

+  method n()

+    requires acc(F) && acc(this.G);

+    ensures acc(F) && acc(G);

+    ensures F == old(G) && G == old(F);

+  {

+    var tmp := F;

+    F := G;

+    G := tmp;

+  }

+}