diff options
| author |  Rustan Leino <unknown> | 2013-12-18 11:31:32 -0800 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2013-12-18 11:31:32 -0800 |
| commit | 886b88e644d1cbb564383c67f3b7935f62e8ef9b (patch) | |
| tree | 2c317dce0ed14f30557ec5e03de3223d8f407a2c /Test/dafny3 | |
| parent | 42d8a89ea406dc001dfd83af2e2d66f5ed813cc7 (diff) | |
Added missing file (sorry)
Diffstat (limited to 'Test/dafny3')
| -rw-r--r-- | Test/dafny3/OpaqueTrees.dfy | 40 |
1 files changed, 40 insertions, 0 deletions
diff --git a/Test/dafny3/OpaqueTrees.dfy b/Test/dafny3/OpaqueTrees.dfy new file mode 100644 index 00000000..a08d0b68 --- /dev/null +++ b/Test/dafny3/OpaqueTrees.dfy @@ -0,0 +1,40 @@ +datatype Tree<T> = Leaf(T) | Node(Tree, Tree)
+
+function {:opaque} size(t: Tree): nat
+{
+ match t
+ case Leaf(_) => 1
+ case Node(left, right) => 1 + size(left) + size(right)
+}
+
+function {:opaque} mirror(t: Tree): Tree
+{
+ match t
+ case Leaf(_) => t
+ case Node(left, right) => Node(mirror(right), mirror(left))
+}
+
+lemma {:induction false} MirrorSize(t: Tree)
+ ensures size(mirror(t)) == size(t);
+{
+ match t {
+ case Leaf(x) =>
+ calc {
+ size(mirror(Leaf(x)));
+ == { reveal_mirror(); }
+ size(Leaf(x));
+ }
+ case Node(left, right) =>
+ calc {
+ size(mirror(Node(left, right)));
+ == { reveal_mirror(); }
+ size(Node(mirror(right), mirror(left)));
+ == { reveal_size(); }
+ 1 + size(mirror(right)) + size(mirror(left));
+ == { MirrorSize(right); MirrorSize(left); } // induction hypothesis
+ 1 + size(right) + size(left);
+ == { reveal_size(); }
+ size(Node(left, right));
+ }
+ }
+}
|