Chalice: added finite differencing refinement

4 files changed, 54 insertions, 49 deletions

diff --git a/Chalice/examples/refinement/FiniteDiff.chalice b/Chalice/examples/refinement/FiniteDiff.chalice
deleted file mode 100644
index ba9dfeb3..00000000
--- a/Chalice/examples/refinement/FiniteDiff.chalice
+++ /dev/null
@@ -1,49 +0,0 @@
-// 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:int) returns (v: int)
-    requires n >= 0; 
-    ensures v == n*n*n;
-  {
-    assume v == n*n*n;
-  }
-}
-
-class Cube1 {
-  method compute(n:int) returns (v: int, w:int) // introducing recursion-local state?
-    requires n >= 0;
-    ensures v == n*n*n;
-    ensures w == (n+1)*(n+1)*(n+1)-n*n*n; // strengthen post-condition
-  {
-    if (n == 0) {
-      v := 0;
-      w := 1;
-    } else {
-      call v1,w1 := compute(n-1); // rely on stronger post-condition
-      v := v1 + w1;
-      assume w == 3*n*n + 3*n + 1; // simplify and guess next step
-    }
-  }
-}
-
-class Cube2 {
-  method compute(n:int) returns (v: int, w:int, x:int) // more state
-    requires n >= 0;
-    ensures v == n*n*n;
-    ensures w == (n+1)*(n+1)*(n+1)-n*n*n;
-    ensures x == (n+1)*(n+1); // stop it here; \delta w is messy
-  { 
-    if (n == 0) {
-      v := 0;
-      w := 1;
-      x := 1;
-    } else {
-      call v1,w1,x1 := compute(n-1);
-      v := v1 + w1;
-      w := 3*x1 + 3*n + 1;
-      x := x1 + 2*n + 1;
-    }
-  }
-} 
diff --git a/Chalice/refinements/Answer b/Chalice/refinements/Answer
index 52a7d06b..0183b442 100644
--- a/Chalice/refinements/Answer
+++ b/Chalice/refinements/Answer
@@ -19,3 +19,6 @@ Boogie program verifier finished with 10 verified, 0 errors
 Processing TestRefines.chalice
 

 Boogie program verifier finished with 9 verified, 0 errors

+Processing RecFiniteDiff.chalice
+

+Boogie program verifier finished with 9 verified, 0 errors

diff --git a/Chalice/refinements/RecFiniteDiff.chalice b/Chalice/refinements/RecFiniteDiff.chalice
new file mode 100644
index 00000000..8fca8d9b
--- /dev/null
+++ b/Chalice/refinements/RecFiniteDiff.chalice
@@ -0,0 +1,50 @@
+// 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;
+      }
+    }
+  }
+} 
diff --git a/Chalice/refinements/test.sh b/Chalice/refinements/test.sh
index 9cc84d90..a9ac7b82 100644
--- a/Chalice/refinements/test.sh
+++ b/Chalice/refinements/test.sh
@@ -7,6 +7,7 @@ TESTS="
   SumCubes.chalice
   TestTransform.chalice
   TestRefines.chalice
+  RecFiniteDiff.chalice
 "
 if [ -f Output ]
 then