Chalice: added finite differencing refinement

1 files changed, 0 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;
-    }
-  }
-}