Dafny: added Carrol Morgan's calculator regression test.

4 files changed, 125 insertions, 54 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 15986246..c56c2aeb 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -448,6 +448,6 @@ Dafny program verifier finished with 10 verified, 0 errors
 

 Dafny program verifier finished with 5 verified, 0 errors

 

--------------------- Counter.dfy --------------------

+-------------------- Refinement.dfy --------------------

 

-Dafny program verifier finished with 22 verified, 0 errors

+Dafny program verifier finished with 39 verified, 0 errors

diff --git a/Test/dafny0/Counter.dfy b/Test/dafny0/Counter.dfy
deleted file mode 100644
index 63f2fc3c..00000000
--- a/Test/dafny0/Counter.dfy
+++ /dev/null
@@ -1,51 +0,0 @@
-// Concrete language syntax for a Dafny extension with refinement. 
-// 6/28/2010
-
-class A { 
-  var n : int;
-    
-  method Init() modifies this; 
-  { n := 0;}
-
-  method Inc() modifies this; 
-  { n := n + 1;}
-
-  method Dec() 
-    modifies this;
-    requires n > 0; 
-  { n := n - 1;}  
-  
-  method Test1(p: int) returns (i: int) 
-  {   
-    assume true;
-  }
-
-  method Test2() returns (o: object)
-  { o := this; }
-}
-
-class B refines A {
-  var inc : int, dec : int;
-    
-  replaces n by n == inc - dec;
-  // transforms n into inc - dec;
-    
-  refines Init() modifies this;
-  { inc := 0; dec := 0;}
-    
-  refines Inc() modifies this;
-  { inc := inc + 1; }  
-  
-  refines Dec() 
-    modifies this;
-    requires inc > dec; 
-  { dec := dec + 1; }
-
-  refines Test1(p: int) returns (i: int) 
-  {
-    i := p;
-  }
-}
-
-    
-    
diff --git a/Test/dafny0/Refinement.dfy b/Test/dafny0/Refinement.dfy
new file mode 100644
index 00000000..c70df916
--- /dev/null
+++ b/Test/dafny0/Refinement.dfy
@@ -0,0 +1,122 @@
+// Concrete language syntax for a Dafny extension with refinement. 
+// Counter example.
+// 6/28/2010
+
+class A { 
+  var n : int;
+    
+  method Init() modifies this; 
+  { n := 0;}
+
+  method Inc() modifies this; 
+  { n := n + 1;}
+
+  method Dec() 
+    modifies this;
+    requires n > 0; 
+  { n := n - 1;}  
+  
+  method Test1(p: int) returns (i: int) 
+  {   
+    assume true;
+  }
+
+  method Test2() returns (o: object)
+  { o := this; }
+}
+
+class B refines A {
+  var inc : int, dec : int;
+    
+  replaces n by n == inc - dec;
+  // transforms n into inc - dec;
+    
+  refines Init() modifies this;
+  { inc := 0; dec := 0;}
+    
+  refines Inc() modifies this;
+  { inc := inc + 1; }  
+  
+  refines Dec() 
+    modifies this;
+    requires inc > dec; 
+  { dec := dec + 1; }
+
+  refines Test1(p: int) returns (i: int) 
+  {
+    i := p;
+  }
+}
+
+// Carrol Morgan's calculator
+// 7/2/2010 Kuat
+
+class ACalc {
+  var vals: seq<int>;
+  
+  method reset() 
+    modifies this;
+  {
+    vals := [];
+  }
+  
+  method add(x: int) 
+    modifies this;
+  {
+    vals := [x] + vals;
+  }
+  
+  method mean() returns (m: int)     
+    requires |vals| > 0;
+  {
+    m := seqsum(vals)/|vals|;
+  }
+
+  static function method seqsum(x:seq<int>) : int
+    decreases x;
+  {
+    if (x == []) then 0 else x[0] + seqsum(x[1..])
+  }
+}
+
+
+class CCalc refines ACalc {
+  var sum: int;
+  var num: int;
+  replaces vals by sum == seqsum2(vals) && num == |vals|;
+
+  refines reset() 
+    modifies this;
+  {
+    sum := 0;
+    num := 0;
+  }
+
+  refines add(x: int)
+    modifies this;
+  {
+    sum := sum + x;
+    num := num + 1;
+  }
+
+  refines mean() returns (m: int)
+    requires num > 0;
+  {
+    m := sum/num;
+  }
+
+  static function method seqsum2(x:seq<int>) : int
+    decreases x;
+  {
+    if (x == []) then 0 else x[0] + seqsum2(x[1..])
+  }
+}
+
+
+
+
+
+
+
+    
+    
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index 8913e626..e238f082 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -14,7 +14,7 @@ for %%f in (Simple.dfy) do (
 for %%f in (TypeTests.dfy SmallTests.dfy Definedness.dfy Array.dfy

             Modules0.dfy Modules1.dfy BadFunction.dfy

             Termination.dfy Use.dfy DTypes.dfy

-            TypeParameters.dfy Datatypes.dfy SplitExpr.dfy Counter.dfy) do (

+            TypeParameters.dfy Datatypes.dfy SplitExpr.dfy Refinement.dfy) do (

   echo.

   echo -------------------- %%f --------------------

   %DAFNY_EXE% /compile:0 %* %%f