Merge

1 files changed, 43 insertions, 0 deletions

diff --git a/Chalice/tests/refinements/LoopSqRoot.chalice b/Chalice/tests/refinements/LoopSqRoot.chalice
new file mode 100644
index 00000000..4ea9434d
--- /dev/null
+++ b/Chalice/tests/refinements/LoopSqRoot.chalice
@@ -0,0 +1,43 @@
+class A0 {
+  method sqroot(n) returns (x)
+    requires n >= 0;
+  { 
+    var x [x*x <= n && n < (x+1)*(x+1) && x >=0];    
+  }
+}
+
+class A1 refines A0 {
+  transforms sqroot(n) returns (x)
+  {
+    replaces x by {
+      var l := 0;
+      var r := n + 1;
+      while (l + 1 != r) 
+        invariant l >= 0 && r > l;
+        invariant l*l <= n && n < r*r;
+      {
+        var k [l < k && k < r];
+        if (k*k <= n) {
+          l := k;
+        } else {
+          r := k;
+        }
+      }
+      x := l;      
+    }
+  }
+}
+
+class A2 refines A1 {
+  transforms sqroot(n) returns (x)
+  {
+    _
+    while {
+      replaces k by {
+        var k [2*k <= l+r && l+r < 2*(k+1)]        
+      }
+      *
+    }
+    _
+  }
+}