From acd37aa3a30c31df6a2c6787a5ac76e9a4e64f1c Mon Sep 17 00:00:00 2001
From: kyessenov <unknown>
Date: Thu, 19 Aug 2010 09:19:36 +0000
Subject: Chalice: added finite differencing refinement

---
 Chalice/examples/refinement/FiniteDiff.chalice | 49 --------------------------
 1 file changed, 49 deletions(-)
 delete mode 100644 Chalice/examples/refinement/FiniteDiff.chalice

(limited to 'Chalice/examples')

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;
-    }
-  }
-} 
-- 
cgit v1.2.3