diff options
| author |  rustanleino <unknown> | 2010-06-08 18:05:23 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-06-08 18:05:23 +0000 |
| commit | 2e8f477b81b1c5c6d3c3f600abac3874548a9e4d (patch) | |
| tree | 03e89bdb4df3a689b7217c5e913557c5b6c6df99 /Test/dafny1/TreeDatatype.dfy | |
| parent | 22e67dc18705c19b617678358c8e859349938ac3 (diff) | |
Boogie:
* Look for Z3 versions up to 2.15 (but did not implement a better algorithm for it).
* Added prover-path output as part of /trace flag (that probably isn't the best command-line option for it).
Dafny:
* Split off some tests from Test/dafny0 into Test/dafny1.
* Added Test/dafny1/UltraFilter.dfy.
Diffstat (limited to 'Test/dafny1/TreeDatatype.dfy')
| -rw-r--r-- | Test/dafny1/TreeDatatype.dfy | 72 |
1 files changed, 72 insertions, 0 deletions
diff --git a/Test/dafny1/TreeDatatype.dfy b/Test/dafny1/TreeDatatype.dfy new file mode 100644 index 00000000..58124171 --- /dev/null +++ b/Test/dafny1/TreeDatatype.dfy @@ -0,0 +1,72 @@ +// ------------------ generic list, non-generic tree
+
+datatype List<T> {
+ Nil;
+ Cons(T, List<T>);
+}
+
+datatype Tree {
+ Node(int, List<Tree>);
+}
+
+static function Inc(t: Tree): Tree
+ decreases t;
+{
+ match t
+ case Node(n, children) => #Tree.Node(n+1, ForestInc(children))
+}
+
+static function ForestInc(forest: List<Tree>): List<Tree>
+ decreases forest;
+{
+ match forest
+ case Nil => forest
+ case Cons(tree, tail) => #List.Cons(Inc(tree), ForestInc(tail))
+}
+
+// ------------------ generic list, generic tree (but GInc defined only for GTree<int>
+
+datatype GTree<T> {
+ Node(T, List<GTree<T>>);
+}
+
+static function GInc(t: GTree<int>): GTree<int>
+ decreases t;
+{
+ match t
+ case Node(n, children) => #GTree.Node(n+1, GForestInc(children))
+}
+
+static function GForestInc(forest: List<GTree<int>>): List<GTree<int>>
+ decreases forest;
+{
+ match forest
+ case Nil => forest
+ case Cons(tree, tail) => #List.Cons(GInc(tree), GForestInc(tail))
+}
+
+// ------------------ non-generic structures
+
+datatype TreeList {
+ Nil;
+ Cons(OneTree, TreeList);
+}
+
+datatype OneTree {
+ Node(int, TreeList);
+}
+
+static function XInc(t: OneTree): OneTree
+ decreases t;
+{
+ match t
+ case Node(n, children) => #OneTree.Node(n+1, XForestInc(children))
+}
+
+static function XForestInc(forest: TreeList): TreeList
+ decreases forest;
+{
+ match forest
+ case Nil => forest
+ case Cons(tree, tail) => #TreeList.Cons(XInc(tree), XForestInc(tail))
+}
|