Added some test cases: theorem about infinite and finite trees.

1 files changed, 2 insertions, 2 deletions

diff --git a/Test/dafny3/WideTrees.dfy b/Test/dafny3/WideTrees.dfy
index 082cdc37..e381726e 100644
--- a/Test/dafny3/WideTrees.dfy
+++ b/Test/dafny3/WideTrees.dfy
@@ -13,7 +13,7 @@ function BigTrees(): Stream<Tree>
 }

 

 // say whether a tree has finite height

-predicate IsFiniteHeight(t: Tree)

+predicate HasBoundedHeight(t: Tree)

 {

   exists n :: 0 <= n && LowerThan(t.children, n)

 }

@@ -37,7 +37,7 @@ function SmallTrees(n: nat): Stream<Tree>
 }

 // prove that the tree returned by SmallTree is finite

 ghost method Theorem(n: nat)

-  ensures IsFiniteHeight(SmallTree(n));

+  ensures HasBoundedHeight(SmallTree(n));

 {

   Lemma(n);

 }