From f175621489a3134089a77f8ae91cc788d8aee6ed Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Wed, 10 Jul 2013 18:32:07 -0700
Subject: Added some test cases having to do with finite/infinite trees

---
 Test/dafny3/Answer        |  4 ++++
 Test/dafny3/WideTrees.dfy | 50 +++++++++++++++++++++++++++++++++++++++++++++++
 Test/dafny3/runtest.bat   |  2 +-
 3 files changed, 55 insertions(+), 1 deletion(-)
 create mode 100644 Test/dafny3/WideTrees.dfy

(limited to 'Test/dafny3')

diff --git a/Test/dafny3/Answer b/Test/dafny3/Answer
index 6ca8aafa..d31b89cc 100644
--- a/Test/dafny3/Answer
+++ b/Test/dafny3/Answer
@@ -46,3 +46,7 @@ Dafny program verifier finished with 28 verified, 0 errors
 -------------------- Filter.dfy --------------------
 
 Dafny program verifier finished with 43 verified, 0 errors
+
+-------------------- WideTrees.dfy --------------------
+
+Dafny program verifier finished with 10 verified, 0 errors
diff --git a/Test/dafny3/WideTrees.dfy b/Test/dafny3/WideTrees.dfy
new file mode 100644
index 00000000..082cdc37
--- /dev/null
+++ b/Test/dafny3/WideTrees.dfy
@@ -0,0 +1,50 @@
+codatatype Stream<T> = SNil | SCons(head: T, tail: Stream)
+datatype Tree = Node(children: Stream<Tree>)
+
+// return an infinite stream of trees
+function BigTree(): Tree
+{
+  Node(BigTrees())
+}
+function BigTrees(): Stream<Tree>
+  decreases 0;
+{
+  SCons(BigTree(), BigTrees())
+}
+
+// say whether a tree has finite height
+predicate IsFiniteHeight(t: Tree)
+{
+  exists n :: 0 <= n && LowerThan(t.children, n)
+}
+copredicate LowerThan(s: Stream<Tree>, n: nat)
+{
+  match s
+  case SNil => true
+  case SCons(t, tail) =>
+    1 <= n && LowerThan(t.children, n-1) && LowerThan(tail, n)
+}
+
+// return a finite tree
+function SmallTree(n: nat): Tree
+{
+  Node(SmallTrees(n))
+}
+function SmallTrees(n: nat): Stream<Tree>
+  decreases -1;
+{
+  if n == 0 then SNil else SCons(SmallTree(n-1), SmallTrees(n))
+}
+// prove that the tree returned by SmallTree is finite
+ghost method Theorem(n: nat)
+  ensures IsFiniteHeight(SmallTree(n));
+{
+  Lemma(n);
+}
+comethod Lemma(n: nat)
+  ensures LowerThan(SmallTrees(n), n);
+{
+  if 0 < n {
+    Lemma(n-1);
+  }
+}
diff --git a/Test/dafny3/runtest.bat b/Test/dafny3/runtest.bat
index c2182d6c..fdf4a152 100644
--- a/Test/dafny3/runtest.bat
+++ b/Test/dafny3/runtest.bat
@@ -8,7 +8,7 @@ for %%f in (
   Iter.dfy Streams.dfy Dijkstra.dfy CachedContainer.dfy
   SimpleInduction.dfy SimpleCoinduction.dfy CalcExample.dfy
   InductionVsCoinduction.dfy Zip.dfy SetIterations.dfy
-  Paulson.dfy Filter.dfy
+  Paulson.dfy Filter.dfy WideTrees.dfy
 ) do (
   echo.
   echo -------------------- %%f --------------------
-- 
cgit v1.2.3