Chalice:

* added loop transform pattern
* implemented translation of refined loops to Boogie (only assert new loop invariants)
* refactored loop target computation code (async call was not handled as maybe some other statement)

1 files changed, 38 insertions, 0 deletions

diff --git a/Chalice/refinements/TestTransform.chalice b/Chalice/refinements/TestTransform.chalice
new file mode 100644
index 00000000..2c18907f
--- /dev/null
+++ b/Chalice/refinements/TestTransform.chalice
@@ -0,0 +1,38 @@
+class A {
+  method m(i: int) returns (x: int) 
+    ensures x == i;
+  {
+    var j := 0;
+    var v [v == i + j];
+    x := v;
+  }
+
+  method n() {
+    var x := 0;
+    var y := 1;
+    var z := 2;  
+  }
+}
+
+class B refines A {
+  transforms m(i: int) returns (x: int, y: int)  
+    ensures y == 0;
+  {
+    var t := 0;
+    _
+    replaces v by {
+      var v := i + j; 
+      call t, j := m(0);
+      y := j;
+    }
+    _
+  }
+
+  transforms n() {
+    replaces * by {
+      var x := 0;
+      var y := x + 1;
+      var z := 2*y;
+    }
+  }
+}