summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar kyessenov <unknown>2010-07-02 18:56:50 +0000
committerGravatar kyessenov <unknown>2010-07-02 18:56:50 +0000
commit8f60fee050c6f7912135327d1dc99b3da4c0ecc4 (patch)
tree7c85f673013fc92cdbf978775f82d9a98ea40188
parent8680b6fec730fd740474d3d06ae80c7d4d6a21c4 (diff)
Dafny: added a regression test for the refinement extension.
-rw-r--r--Test/dafny0/Answer4
-rw-r--r--Test/dafny0/Counter.dfy44
-rw-r--r--Test/dafny0/runtest.bat2
3 files changed, 49 insertions, 1 deletions
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