diff options
| author |  Rustan Leino <unknown> | 2013-07-10 18:32:07 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2013-07-10 18:32:07 -0700 |
| commit | f175621489a3134089a77f8ae91cc788d8aee6ed (patch) | |
| tree | 31a314b164be665ccf19eccbf1dbd89e5e50c010 /Test/dafny3 | |
| parent | 8e467cdab8f3de3933a0cfbe372520225adcc97d (diff) | |
Added some test cases having to do with finite/infinite trees
Diffstat (limited to 'Test/dafny3')
| -rw-r--r-- | Test/dafny3/Answer | 4 | ||||
| -rw-r--r-- | Test/dafny3/WideTrees.dfy | 50 | ||||
| -rw-r--r-- | Test/dafny3/runtest.bat | 2 |
3 files changed, 55 insertions, 1 deletions
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 --------------------
|