1 files changed, 0 insertions, 51 deletions
diff --git a/Chalice/tests/refinements/RecFiniteDiff.chalice b/Chalice/tests/refinements/RecFiniteDiff.chalice
deleted file mode 100644
index 1a971aed..00000000
--- a/Chalice/tests/refinements/RecFiniteDiff.chalice
+++ /dev/null
@@ -1,51 +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) 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;
-      }
-    }
-  }
-}