Merge

1 files changed, 51 insertions, 0 deletions

diff --git a/Chalice/tests/refinements/RecFiniteDiff.chalice b/Chalice/tests/refinements/RecFiniteDiff.chalice
new file mode 100644
index 00000000..1a971aed
--- /dev/null
+++ b/Chalice/tests/refinements/RecFiniteDiff.chalice
@@ -0,0 +1,51 @@
+// Example of a program computing cube using only addition. 
+// Step-wise refinement using specification statement. 
+// Chalice does not have termination metric for recursive methods.
+
+class Cube0 {
+  method compute(n) returns (v)
+    requires n >= 0; 
+    ensures v == n*n*n;
+  {
+    var v [v == n*n*n]
+  }
+}
+
+class Cube1 refines Cube0 {
+  transforms compute(n) returns (v, w) 
+    // strengthen post-condition based on new output variables
+    ensures w == (n+1)*(n+1)*(n+1)-n*n*n; 
+  {
+    replaces v by {
+      if (n == 0) {
+        v := 0;
+        w := 1;
+      } else {
+        call v1,w1 := compute(n-1); // rely on stronger post-condition
+        v := v1 + w1;
+        // simplified form: aha! we need n*n to compute with addition
+        var w [w == 3*n*n + 3*n + 1];
+      }
+    }
+  }
+}
+
+class Cube2 refines Cube1 {
+  transforms compute(n) returns (v, w, x) 
+    ensures x == (n+1)*(n+1);   
+  { 
+    if {
+      _
+      x := 1;
+    } else {
+      replaces v1, w1 by {
+        call v1,w1,x1 := compute(n-1);
+      }
+      _
+      replaces w by {
+        w := 3*x1 + 3*n + 1;
+        x := x1 + 2*n + 1;
+      }
+    }
+  }
+}