1 files changed, 93 insertions, 0 deletions
diff --git a/Chalice/tests/examples/prog2.chalice b/Chalice/tests/examples/prog2.chalice
new file mode 100644
index 00000000..55fe8ff5
--- /dev/null
+++ b/Chalice/tests/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
+  }
+}