Merge

1 files changed, 35 insertions, 0 deletions

diff --git a/Chalice/tests/refinements/SpecStmt.chalice b/Chalice/tests/refinements/SpecStmt.chalice
new file mode 100644
index 00000000..15072d41
--- /dev/null
+++ b/Chalice/tests/refinements/SpecStmt.chalice
@@ -0,0 +1,35 @@
+class Test {
+  var x: int;
+  method m(a:int) returns (b:int) 
+  {
+    var c := 0;
+    ghost const d,c [d == c];
+    var b [b == 0];  
+    var e [e == a];   
+    assert d == c;
+    assert e == a;
+    assert b == 0;
+    assert c == 0; // error 
+  }
+
+  method n() 
+    requires acc(x);
+  {
+    x := 0;
+    const y [acc(x), rd(x) && x == old(x) + 1 && y == x];
+    assert y == 1;
+    const v [rd(x), rd(x) && v == old(x) + 1];
+    assert v == 2;
+    const z [z == 1];
+    ghost var t [z == 1, true];     
+    assert false; // reachable 
+  }
+
+  method o()  
+  {
+    var z [acc(x) && z == 0]; // unimplementable
+    x := z;
+    assert x == 0;
+    assert false; // reachable
+  }
+}