From 8f60fee050c6f7912135327d1dc99b3da4c0ecc4 Mon Sep 17 00:00:00 2001
From: kyessenov <unknown>
Date: Fri, 2 Jul 2010 18:56:50 +0000
Subject: Dafny: added a regression test for the refinement extension.

---
 Test/dafny0/Answer      |  4 ++++
 Test/dafny0/Counter.dfy | 44 ++++++++++++++++++++++++++++++++++++++++++++
 Test/dafny0/runtest.bat |  2 +-
 3 files changed, 49 insertions(+), 1 deletion(-)
 create mode 100644 Test/dafny0/Counter.dfy

(limited to 'Test')

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 0581fe6b..2577557a 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -447,3 +447,7 @@ Dafny program verifier finished with 10 verified, 0 errors
 -------------------- SplitExpr.dfy --------------------
 
 Dafny program verifier finished with 5 verified, 0 errors
+
+-------------------- Counter.dfy --------------------
+
+Dafny program verifier finished with 19 verified, 0 errors
diff --git a/Test/dafny0/Counter.dfy b/Test/dafny0/Counter.dfy
new file mode 100644
index 00000000..c38b28dc
--- /dev/null
+++ b/Test/dafny0/Counter.dfy
@@ -0,0 +1,44 @@
+// 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() returns (i: int) 
+  { i := 0;}
+
+  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; }
+}
+
+    
+    
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index 0e8146c0..8913e626 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) do (
+            TypeParameters.dfy Datatypes.dfy SplitExpr.dfy Counter.dfy) do (
   echo.
   echo -------------------- %%f --------------------
   %DAFNY_EXE% /compile:0 %* %%f
-- 
cgit v1.2.3