1 files changed, 109 insertions, 0 deletions
diff --git a/Chalice/tests/examples/prog0.chalice b/Chalice/tests/examples/prog0.chalice
new file mode 100644
index 00000000..fb835a24
--- /dev/null
+++ b/Chalice/tests/examples/prog0.chalice
@@ -0,0 +1,109 @@
+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 waitlevel;
+  }
+  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 { }
+
+// ----- tests specifically of implicit locals in CALL and RECEIVE statements
+
+class ImplicitC {
+  var k: int;
+
+  method MyMethod() returns (x: int, y: ImplicitC)
+    requires acc(k)
+    ensures acc(y.k) && x < y.k
+  {
+    x := k - 15;
+    y := this;
+  }
+
+  method B0() {
+    var c := new ImplicitC;
+    call a, b := c.MyMethodX();  // error: method not found (so what is done with a,b?)
+    assert a < b.k;
+  }
+
+  method B1() {
+    var c := new ImplicitC;
+    call a, a := c.MyMethod();  // error: a occurs twice
+    assert a < b.k;
+  }
+
+  method D0() {
+    var ch := new Ch;
+    var c := new ImplicitC;
+    send ch(c.k - 15, c);  // give ourselves some credit
+    receive a, b := chX;  // error: channel not found (so what is done with a,b?)
+    assert a < b.k;
+  }
+
+  method D1() {
+    var ch := new Ch;
+    var c := new ImplicitC;
+    send ch(c.k - 15, c);  // give ourselves some credit
+    receive a, a := ch;  // error: a occurs twice
+    assert a < b.k;
+  }
+}
+
+channel Ch(x: int, y: ImplicitC) where acc(y.k) && x < y.k;