1 files changed, 65 insertions, 0 deletions
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 { }