1 files changed, 0 insertions, 69 deletions
diff --git a/Chalice/tests/refinements/Calculator.chalice b/Chalice/tests/refinements/Calculator.chalice
deleted file mode 100644
index 57c4c87d..00000000
--- a/Chalice/tests/refinements/Calculator.chalice
+++ /dev/null
@@ -1,69 +0,0 @@
-/*
-  Carrol Morgan's calculator  
-  7/2/2010 Kuat Dafny version
-  8/22/2010 translated into Chalice
-*/ 
-
-class Calc0 {  
-  var vals: seq<int>;
-  
-  method reset() 
-    requires acc(vals);
-    ensures acc(vals);
-  {
-    vals := [];
-  }
-  
-  method add(x: int) 
-    requires acc(vals);
-    ensures acc(vals);
-  {
-    vals := [x] ++ vals;    
-  }
-  
-  method mean() returns (m: int)     
-    requires acc(vals) && |vals| > 0;
-    ensures acc(vals);
-  {
-    m := total(vals)/|vals|;
-  }
-
-  unlimited function total(s: seq<int>): int
-  {
-    |s| == 0 ? 0 : s[0] + total(s[1..])
-  }  
-}
-
-
-
-class Calc1 refines Calc0 {  
-  var sum: int;
-  var num: int;
-  replaces vals by acc(sum) && acc(num) && sum == total(vals) && num == |vals|;
-
-  refines reset()   
-  {
-    sum := 0;
-    num := 0;
-  }
-
-  refines add(x: int)    
-  {
-    sum := sum + x;
-    num := num + 1;
-  }
-
-  refines mean() returns (m: int)  
-  {
-    m := sum/num;
-  }
-}
-
-
-
-
-
-
-
-    
-