From fb6c171957142ce6119a7363d3cec66799b9966a Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Sat, 27 Jul 2013 08:15:50 -0700 Subject: Added some test cases: theorem about infinite and finite trees. --- Test/dafny3/Answer | 4 + Test/dafny3/InfiniteTrees.dfy | 710 ++++++++++++++++++++++++++++++++++++++++++ Test/dafny3/WideTrees.dfy | 4 +- Test/dafny3/runtest.bat | 2 +- 4 files changed, 717 insertions(+), 3 deletions(-) create mode 100644 Test/dafny3/InfiniteTrees.dfy (limited to 'Test/dafny3') diff --git a/Test/dafny3/Answer b/Test/dafny3/Answer index d31b89cc..f326d2f9 100644 --- a/Test/dafny3/Answer +++ b/Test/dafny3/Answer @@ -50,3 +50,7 @@ Dafny program verifier finished with 43 verified, 0 errors -------------------- WideTrees.dfy -------------------- Dafny program verifier finished with 10 verified, 0 errors + +-------------------- InfiniteTrees.dfy -------------------- + +Dafny program verifier finished with 88 verified, 0 errors diff --git a/Test/dafny3/InfiniteTrees.dfy b/Test/dafny3/InfiniteTrees.dfy new file mode 100644 index 00000000..e189dc4a --- /dev/null +++ b/Test/dafny3/InfiniteTrees.dfy @@ -0,0 +1,710 @@ +// Here is the usual definition of possibly infinite lists, along with a function Tail(s, n), which drops +// n heads from s, and two lemmas that prove properties of Tail. + +codatatype Stream = Nil | Cons(head: T, tail: Stream) + +function Tail(s: Stream, n: nat): Stream +{ + if n == 0 then s else + var t := Tail(s, n-1); + if t == Nil then t else t.tail +} + +ghost method Tail_Lemma0(s: Stream, n: nat) + requires s.Cons? && Tail(s, n).Cons?; + ensures Tail(s, n).tail == Tail(s.tail, n); +{ +} +ghost method Tail_Lemma1(s: Stream, k: nat, n: nat) + requires k <= n; + ensures Tail(s, n).Cons? ==> Tail(s, k).Cons?; + // Note, the contrapositive of this lemma says: Tail(s, k) == Nil ==> Tail(s, n) == Nil +{ + if k < n && Tail(s, n).Cons? { + assert Tail(s, n) == Tail(s, n-1).tail; + } +} +ghost method Tail_Lemma2(s: Stream, n: nat) + requires s.Cons? && Tail(s.tail, n).Cons?; + ensures Tail(s, n).Cons?; +{ + if n != 0 { + Tail_Lemma0(s, n-1); + } +} + +// Co-predicate IsNeverEndingStream(s) answers whether or not s ever contains Nil. + +copredicate IsNeverEndingStream(s: Stream) +{ + match s + case Nil => false + case Cons(_, tail) => IsNeverEndingStream(tail) +} + +// Here is an example of an infinite stream. + +function AnInfiniteStream(): Stream +{ + Cons(0, AnInfiniteStream()) +} +comethod Proposition0() + ensures IsNeverEndingStream(AnInfiniteStream()); +{ +} + +// Now, consider a Tree definition, where each node can have a possibly infinite number of children. + +datatype Tree = Node(children: Stream) + +// Such a tree might have not just infinite width but also infinite height. The following predicate +// holds if there is, for every path down from the root, a common bound on the height of each such path. +// Note that the definition needs a co-predicate in order to say something about all of a node's children. + +predicate HasBoundedHeight(t: Tree) +{ + exists n :: 0 <= n && LowerThan(t.children, n) +} +copredicate LowerThan(s: Stream, n: nat) +{ + match s + case Nil => true + case Cons(t, tail) => + 1 <= n && LowerThan(t.children, n-1) && LowerThan(tail, n) +} + +// Co-predicate LowerThan(s, n) recurses on LowerThan(s.tail, n). Thus, a property of LowerThan is that +// LowerThan(s, h) implies LowerThan(s', h) for any suffix s' of s. + +ghost method LowerThan_Lemma(s: Stream, n: nat, h: nat) + ensures LowerThan(s, h) ==> LowerThan(Tail(s, n), h); +{ + Tail_Lemma1(s, 0, n); + if n == 0 || Tail(s, n) == Nil { + } else { + match s { + case Cons(t, tail) => + LowerThan_Lemma(tail, n-1, h); + Tail_Lemma0(s, n-1); + } + } +} + +// A tree t where every node has an infinite number of children satisfies InfiniteEverywhere(t.children). +// Otherwise, IsFiniteSomewhere(t) holds. That is, IsFiniteSomewhere says that the tree has some node +// with less than infinite width. Such a tree may or may not be of finite height, as we'll see in an +// example below. + +predicate IsFiniteSomewhere(t: Tree) +{ + !InfiniteEverywhere(t.children) +} +copredicate InfiniteEverywhere(s: Stream) +{ + match s + case Nil => false + case Cons(t, tail) => InfiniteEverywhere(t.children) && InfiniteEverywhere(tail) +} + +// Here is a tree where every node has exactly 1 child. Such a tree is finite in width (which implies +// it is finite somewhere) and infinite in height (which implies there is no bound on its height). + +function SkinnyTree(): Tree +{ + Node(Cons(SkinnyTree(), Nil)) +} +ghost method Proposition1() + ensures IsFiniteSomewhere(SkinnyTree()) && !HasBoundedHeight(SkinnyTree()); +{ + assert forall n :: 0 <= n ==> !LowerThan(SkinnyTree().children, n); +} + +// Any tree where all paths have bounded height are finite somewhere. + +ghost method Theorem0(t: Tree) + requires HasBoundedHeight(t); + ensures IsFiniteSomewhere(t); +{ + var n :| 0 <= n && LowerThan(t.children, n); + /* + assert (forall k :: 0 <= k ==> InfiniteEverywhere#[k](t.children)) ==> InfiniteEverywhere(t.children); + assert InfiniteEverywhere(t.children) ==> (forall k :: 0 <= k ==> InfiniteEverywhere#[k](t.children)); + assert InfiniteEverywhere(t.children) <==> (forall k :: 0 <= k ==> InfiniteEverywhere#[k](t.children)); // TODO: why does this not follow from the previous two? + */ + var k := FindNil(t.children, n); +} +ghost method FindNil(s: Stream, n: nat) returns (k: nat) + requires LowerThan(s, n); + ensures !InfiniteEverywhere#[k](s); +{ + match s { + case Nil => k := 1; + case Cons(t, _) => + k := FindNil(t.children, n-1); + k := k + 1; + } +} + +// We defined an InfiniteEverywhere property above and negated it to get an IsFiniteSomewhere predicate. +// If we had an InfiniteHeightSomewhere property, then we could negate it to obtain a predicate +// HasFiniteHeightEverywhere. Consider the following definitions: + +predicate HasFiniteHeightEverywhere_Bad(t: Tree) +{ + !InfiniteHeightSomewhere_Bad(t.children) +} +copredicate InfiniteHeightSomewhere_Bad(s: Stream) +{ + match s + case Nil => false + case Cons(t, tail) => InfiniteHeightSomewhere_Bad(t.children) || InfiniteHeightSomewhere_Bad(tail) +} + +// In some ways, this definition may look reasonable--a list of trees is infinite somewhere +// if it is nonempty, and either the list of children of the first node satisfies the property +// or the tail of the list does. However, because co-predicates are defined by greatest +// fix-points, there is nothing in this definition that "forces" the list to ever get to a +// node whose list of children satisfy the property. The following example shows that a +// shallow, infinitely wide tree satisfies the negation of HasFiniteHeightEverywhere_Bad. + +function ATree(): Tree +{ + Node(ATreeChildren()) +} +function ATreeChildren(): Stream +{ + Cons(Node(Nil), ATreeChildren()) +} +ghost method Proposition2() + ensures !HasFiniteHeightEverywhere_Bad(ATree()); +{ + Proposition2_Lemma0(); + Proposition2_Lemma1(ATreeChildren()); +} +comethod Proposition2_Lemma0() + ensures IsNeverEndingStream(ATreeChildren()); +{ +} +comethod Proposition2_Lemma1(s: Stream) + requires IsNeverEndingStream(s); + ensures InfiniteHeightSomewhere_Bad(s); +{ + calc { + InfiniteHeightSomewhere_Bad#[_k](s); + InfiniteHeightSomewhere_Bad#[_k-1](s.head.children) || InfiniteHeightSomewhere_Bad#[_k-1](s.tail); + <== + InfiniteHeightSomewhere_Bad#[_k-1](s.tail); // induction hypothesis + } +} + +// What was missing from the InfiniteHeightSomewhere_Bad definition was the existence of a child +// node that satisfies the property recursively. To address that problem, we may consider +// a definition like the following: + +/* +predicate HasFiniteHeightEverywhere_Attempt(t: Tree) +{ + !InfiniteHeightSomewhere_Attempt(t.children) +} +copredicate InfiniteHeightSomewhere_Attempt(s: Stream) +{ + exists n :: + 0 <= n && + var ch := Tail(s, n); + ch.Cons? && InfiniteHeightSomewhere_Attempt(ch.head.children) +} +*/ + +// However, Dafny does not allow this definition: the recursive call to InfiniteHeightSomewhere_Attempt +// sits inside an unbounded existential quantifier, which means the co-predicate's connection with its prefix +// predicate is not guaranteed to hold, so Dafny disallows this co-predicate definition. + +// We will use a different way to express the HasFiniteHeightEverywhere property. Instead of +// using an existential quantifier inside the recursively defined co-predicate, we can place a "larger" +// existential quantifier outside the call to the co-predicate. This existential quantifier is going to be +// over the possible paths down the tree (it is "larger" in the sense that it selects a child tree at each +// level down the path, not just at one level). + +// A path is a possibly infinite list of indices, each selecting the next child tree to navigate to. A path +// is valid when it uses valid indices and does not stop at a node with children. + +copredicate ValidPath(t: Tree, p: Stream) +{ + match p + case Nil => t == Node(Nil) + case Cons(index, tail) => + 0 <= index && + var ch := Tail(t.children, index); + ch.Cons? && ValidPath(ch.head, tail) +} +ghost method ValidPath_Lemma(p: Stream) + ensures ValidPath(Node(Nil), p) ==> p == Nil; +{ + if ValidPath(Node(Nil), p) { + match p { + case Nil => + case Cons(index, tail) => // proof by contradiction + Tail_Lemma1(Nil, 0, index); + } + } +} + +// A tree has finite height (everywhere) if it has no valid infinite paths. + +predicate HasFiniteHeight(t: Tree) +{ + forall p :: ValidPath(t, p) ==> !IsNeverEndingStream(p) +} + +// From this definition, we can prove that any tree of bounded height is also of finite height. + +ghost method Theorem1(t: Tree) + requires HasBoundedHeight(t); + ensures HasFiniteHeight(t); +{ + var n :| 0 <= n && LowerThan(t.children, n); + forall p | ValidPath(t, p) { + Theorem1_Lemma(t, n, p); + } +} +ghost method Theorem1_Lemma(t: Tree, n: nat, p: Stream) + requires LowerThan(t.children, n) && ValidPath(t, p); + ensures !IsNeverEndingStream(p); + decreases n; +{ + match p { + case Nil => + case Cons(index, tail) => + var ch := Tail(t.children, index); + calc { + LowerThan(t.children, n); + ==> { LowerThan_Lemma(t.children, index, n); } + LowerThan(ch, n); + ==> // def. LowerThan + LowerThan(ch.head.children, n-1); + ==> { Theorem1_Lemma(ch.head, n-1, tail); } + !IsNeverEndingStream(tail); + ==> // def. IsNeverEndingStream + !IsNeverEndingStream(p); + } + } +} + +// In fact, HasBoundedHeight is strictly strong than HasFiniteHeight, as we'll show with an example. +// Define SkinnyFiniteTree(n) to be a skinny (that is, of width 1) tree of height n. + +function SkinnyFiniteTree(n: nat): Tree + ensures forall k: nat :: LowerThan(SkinnyFiniteTree(n).children, k) <==> n <= k; +{ + if n == 0 then Node(Nil) else Node(Cons(SkinnyFiniteTree(n-1), Nil)) +} + +// Next, we define a tree whose root has an infinite number of children, child i of which +// is a SkinnyFiniteTree(i). + +function FiniteUnboundedTree(): Tree +{ + Node(EverLongerSkinnyTrees(0)) +} +function EverLongerSkinnyTrees(n: nat): Stream +{ + Cons(SkinnyFiniteTree(n), EverLongerSkinnyTrees(n+1)) +} + +ghost method EverLongerSkinnyTrees_Lemma(k: nat, n: nat) + ensures Tail(EverLongerSkinnyTrees(k), n).Cons?; + ensures Tail(EverLongerSkinnyTrees(k), n).head == SkinnyFiniteTree(k+n); + decreases n; +{ + if n == 0 { + } else { + calc { + Tail(EverLongerSkinnyTrees(k), n); + { EverLongerSkinnyTrees_Lemma(k, n-1); } // this ensures that .tail on the next line is well-defined + Tail(EverLongerSkinnyTrees(k), n-1).tail; + { Tail_Lemma0(EverLongerSkinnyTrees(k), n-1); } + Tail(EverLongerSkinnyTrees(k).tail, n-1); + Tail(EverLongerSkinnyTrees(k+1), n-1); + } + EverLongerSkinnyTrees_Lemma(k+1, n-1); + } +} + +ghost method Proposition3() + ensures !HasBoundedHeight(FiniteUnboundedTree()) && HasFiniteHeight(FiniteUnboundedTree()); +{ + Proposition3a(); + Proposition3b(); +} +ghost method Proposition3a() + ensures !HasBoundedHeight(FiniteUnboundedTree()); +{ + var ch := FiniteUnboundedTree().children; + forall n | 0 <= n + ensures !LowerThan(ch, n); + { + var cn := Tail(ch, n+1); + EverLongerSkinnyTrees_Lemma(0, n+1); + assert cn.head == SkinnyFiniteTree(n+1); + assert !LowerThan(cn.head.children, n); + LowerThan_Lemma(ch, n+1, n); + } +} +ghost method Proposition3b() + ensures HasFiniteHeight(FiniteUnboundedTree()); +{ + var t := FiniteUnboundedTree(); + forall p | ValidPath(t, p) + ensures !IsNeverEndingStream(p); + { + assert p.Cons?; + var index := p.head; + assert 0 <= index; + var ch := Tail(t.children, index); + assert ch.Cons? && ValidPath(ch.head, p.tail); + EverLongerSkinnyTrees_Lemma(0, index); + assert ch.head == SkinnyFiniteTree(index); + var si := SkinnyFiniteTree(index); + assert LowerThan(si.children, index); + Proposition3b_Lemma(si, index, p.tail); + } +} +ghost method Proposition3b_Lemma(t: Tree, h: nat, p: Stream) + requires LowerThan(t.children, h) && ValidPath(t, p); + ensures !IsNeverEndingStream(p); + decreases h; +{ + match p { + case Nil => + case Cons(index, tail) => + // From the definition of ValidPath(t, p), we get the following: + var ch := Tail(t.children, index); + assert ch.Cons? && ValidPath(ch.head, tail); + // From the definition of LowerThan(t.children, h), we get the following: + match t.children { + case Nil => + ValidPath_Lemma(p); + assert false; // absurd case + case Cons(_, _) => + assert 1 <= h; + LowerThan_Lemma(t.children, index, h); + assert LowerThan(ch, h); + } + // Putting these together, by ch.Cons? and the definition of LowerThan(ch, h), we get: + assert LowerThan(ch.head.children, h-1); + // And now we can invoke the induction hypothesis: + Proposition3b_Lemma(ch.head, h-1, tail); + } +} + +// Using a stream of integers to denote a path is convenient, because it allows us to +// use Tail to quickly select the next child tree. But we can also define paths in a +// way that more directly follows the navigation steps required to get to the next child, +// using Peano numbers instead of the built-in integers. This means that each Succ +// constructor among the Peano numbers corresponds to moving "right" among the children +// of a tree node. A path is valid only if it always selects a child from a list +// of children; this implies we must avoid infinite "right" moves. The appropriate type +// Numbers (which is really just a stream of natural numbers) is defined as a combination +// two mutually recursive datatypes, one inductive and the other co-inductive. + +codatatype CoOption = None | Some(get: T) +datatype Number = Succ(Number) | Zero(CoOption) + +// Note that the use of an inductive datatype for Number guarantees that sequences of successive +// "right" moves are finite (analogously, each Peano number is finite). Yet the use of a co-inductive +// CoOption in between allows paths to go on forever. In contrast, a definition like: + +codatatype InfPath = Right(InfPath) | Down(InfPath) | Stop + +// does not guarantee the absence of infinitely long sequences of "right" moves. In other words, +// InfPath also gives rise to indecisive paths--those that never select a child node. Also, +// compare the definition of Number with: + +codatatype FinPath = Right(FinPath) | Down(FinPath) | Stop + +// where the type can only represent finite paths. As a final alternative to consider, had we +// wanted only infinite, decisive paths, we would just drop the None constructor, forcing each +// CoOption to be some Number. As it is, we want to allow both finite and infinite paths, but we +// want to be able to distinguish them, so we define a co-predicate that does so: + +copredicate InfinitePath(r: CoOption) +{ + match r + case None => false + case Some(num) => InfinitePath'(num) +} +copredicate InfinitePath'(num: Number) +{ + match num + case Succ(next) => InfinitePath'(next) + case Zero(r) => InfinitePath(r) +} + +// As before, a path is valid for a tree when it navigates to existing nodes and does not stop +// in a node with more children. + +copredicate ValidPath_Alt(t: Tree, r: CoOption) +{ + match r + case None => t == Node(Nil) + case Some(num) => ValidPath_Alt'(t.children, num) +} +copredicate ValidPath_Alt'(s: Stream, num: Number) +{ + match num + case Succ(next) => s.Cons? && ValidPath_Alt'(s.tail, next) + case Zero(r) => s.Cons? && ValidPath_Alt(s.head, r) +} + +// Here is the alternative definition of a tree that has finite height everywhere, using the +// new paths. + +predicate HasFiniteHeight_Alt(t: Tree) +{ + forall r :: ValidPath_Alt(t, r) ==> !InfinitePath(r) +} + +// We will prove that this new definition is equivalent to the previous. To do that, we +// first definite functions S2N and N2S to map between the path representations +// Stream and CoOption, and then prove some lemmas about this correspondence. + +function S2N(p: Stream): CoOption + decreases 0; +{ + match p + case Nil => None + case Cons(n, tail) => Some(S2N'(if n < 0 then 0 else n, tail)) +} +function S2N'(n: nat, tail: Stream): Number + decreases n + 1; +{ + if n <= 0 then Zero(S2N(tail)) else Succ(S2N'(n-1, tail)) +} + +function N2S(r: CoOption): Stream +{ + match r + case None => Nil + case Some(num) => N2S'(0, num) +} +function N2S'(n: nat, num: Number): Stream + decreases num; +{ + match num + case Zero(r) => Cons(n, N2S(r)) + case Succ(next) => N2S'(n + 1, next) +} + +ghost method Path_Lemma0(t: Tree, p: Stream) + requires ValidPath(t, p); + ensures ValidPath_Alt(t, S2N(p)); +{ + if ValidPath(t, p) { + Path_Lemma0'(t, p); + } +} +comethod Path_Lemma0'(t: Tree, p: Stream) + requires ValidPath(t, p); + ensures ValidPath_Alt(t, S2N(p)); +{ + match p { + case Nil => + assert t == Node(Nil); + case Cons(index, tail) => + assert 0 <= index; + var ch := Tail(t.children, index); + assert ch.Cons? && ValidPath(ch.head, tail); + + calc { + ValidPath_Alt#[_k](t, S2N(p)); + { assert S2N(p) == Some(S2N'(index, tail)); } + ValidPath_Alt#[_k](t, Some(S2N'(index, tail))); + // def. ValidPath_Alt# + ValidPath_Alt'#[_k-1](t.children, S2N'(index, tail)); + { Path_Lemma0''(t.children, index, tail); } + true; + } + } +} +comethod Path_Lemma0''(tChildren: Stream, n: nat, tail: Stream) + requires var ch := Tail(tChildren, n); ch.Cons? && ValidPath(ch.head, tail); + ensures ValidPath_Alt'(tChildren, S2N'(n, tail)); +{ + Tail_Lemma1(tChildren, 0, n); + match S2N'(n, tail) { + case Succ(next) => + calc { + Tail(tChildren, n); + { Tail_Lemma1(tChildren, n-1, n); } + Tail(tChildren, n-1).tail; + { Tail_Lemma0(tChildren, n-1); } + Tail(tChildren.tail, n-1); + } + Path_Lemma0''(tChildren.tail, n-1, tail); + case Zero(r) => + Path_Lemma0'(tChildren.head, tail); + } +} +ghost method Path_Lemma1(t: Tree, r: CoOption) + requires ValidPath_Alt(t, r); + ensures ValidPath(t, N2S(r)); +{ + if ValidPath_Alt(t, r) { + Path_Lemma1'(t, r); + } +} +comethod Path_Lemma1'(t: Tree, r: CoOption) + requires ValidPath_Alt(t, r); + ensures ValidPath(t, N2S(r)); + decreases 1; +{ + match r { + case None => + assert t == Node(Nil); + assert N2S(r) == Nil; + case Some(num) => + assert ValidPath_Alt'(t.children, num); + // assert N2S'(0, num).Cons?; + // Path_Lemma1''(t.children, 0, num); + var p := N2S'(0, num); + calc { + ValidPath#[_k](t, N2S(r)); + ValidPath#[_k](t, N2S(Some(num))); + ValidPath#[_k](t, N2S'(0, num)); + { Path_Lemma1''#[_k](t.children, 0, num); } + true; + } + } +} +comethod Path_Lemma1''(s: Stream, n: nat, num: Number) + requires ValidPath_Alt'(Tail(s, n), num); + ensures ValidPath(Node(s), N2S'(n, num)); + decreases 0, num; +{ + match num { + case Succ(next) => + Path_Lemma1''#[_k](s, n+1, next); + case Zero(r) => + calc { + ValidPath#[_k](Node(s), N2S'(n, num)); + ValidPath#[_k](Node(s), Cons(n, N2S(r))); + Tail(s, n).Cons? && ValidPath#[_k-1](Tail(s, n).head, N2S(r)); + { assert Tail(s, n).Cons?; } + ValidPath#[_k-1](Tail(s, n).head, N2S(r)); + { Path_Lemma1'(Tail(s, n).head, r); } + true; + } + } +} +ghost method Path_Lemma2(p: Stream) + ensures IsNeverEndingStream(p) ==> InfinitePath(S2N(p)); +{ + if IsNeverEndingStream(p) { + Path_Lemma2'(p); + } +} +comethod Path_Lemma2'(p: Stream) + requires IsNeverEndingStream(p); + ensures InfinitePath(S2N(p)); +{ + match p { + case Cons(n, tail) => + calc { + InfinitePath#[_k](S2N(p)); + // def. S2N + InfinitePath#[_k](Some(S2N'(if n < 0 then 0 else n, tail))); + // def. InfinitePath + InfinitePath'#[_k-1](S2N'(if n < 0 then 0 else n, tail)); + <== { Path_Lemma2''(p, if n < 0 then 0 else n, tail); } + InfinitePath#[_k-1](S2N(tail)); + { Path_Lemma2'(tail); } + true; + } + } +} +comethod Path_Lemma2''(p: Stream, n: nat, tail: Stream) + requires IsNeverEndingStream(p) && p.tail == tail; + ensures InfinitePath'(S2N'(n, tail)); +{ + if n <= 0 { + calc { + InfinitePath'#[_k](S2N'(n, tail)); + // def. S2N' + InfinitePath'#[_k](Zero(S2N(tail))); + // def. InfinitePath' + InfinitePath#[_k-1](S2N(tail)); + { Path_Lemma2'(tail); } + true; + } + } else { + calc { + InfinitePath'#[_k](S2N'(n, tail)); + // def. S2N' + InfinitePath'#[_k](Succ(S2N'(n-1, tail))); + // def. InfinitePath' + InfinitePath'#[_k-1](S2N'(n-1, tail)); + { Path_Lemma2''(p, n-1, tail); } + true; + } + } +} +ghost method Path_Lemma3(r: CoOption) + ensures InfinitePath(r) ==> IsNeverEndingStream(N2S(r)); +{ + if InfinitePath(r) { + match r { + case Some(num) => Path_Lemma3'(0, num); + } + } +} +comethod Path_Lemma3'(n: nat, num: Number) + requires InfinitePath'(num); + ensures IsNeverEndingStream(N2S'(n, num)); + decreases num; +{ + match num { + case Zero(r) => + calc { + IsNeverEndingStream#[_k](N2S'(n, num)); + // def. N2S' + IsNeverEndingStream#[_k](Cons(n, N2S(r))); + // def. IsNeverEndingStream + IsNeverEndingStream#[_k-1](N2S(r)); + { Path_Lemma3'(0, r.get); } + true; + } + case Succ(next) => + Path_Lemma3'#[_k](n + 1, next); + } +} + +ghost method Theorem2(t: Tree) + ensures HasFiniteHeight(t) <==> HasFiniteHeight_Alt(t); +{ + if HasFiniteHeight_Alt(t) { + forall p { + calc ==> { + ValidPath(t, p); + { Path_Lemma0(t, p); } + ValidPath_Alt(t, S2N(p)); + // assumption HasFiniteHeight(t) + !InfinitePath(S2N(p)); + { Path_Lemma2(p); } + !IsNeverEndingStream(p); + } + } + } + if HasFiniteHeight(t) { + forall r { + calc ==> { + ValidPath_Alt(t, r); + { Path_Lemma1(t, r); } + ValidPath(t, N2S(r)); + // assumption HasFiniteHeight_Alt(t) + !IsNeverEndingStream(N2S(r)); + { Path_Lemma3(r); } + !InfinitePath(r); + } + } + } +} 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 } // 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 } // prove that the tree returned by SmallTree is finite ghost method Theorem(n: nat) - ensures IsFiniteHeight(SmallTree(n)); + ensures HasBoundedHeight(SmallTree(n)); { Lemma(n); } diff --git a/Test/dafny3/runtest.bat b/Test/dafny3/runtest.bat index fdf4a152..7a3d3a20 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 WideTrees.dfy + Paulson.dfy Filter.dfy WideTrees.dfy InfiniteTrees.dfy ) do ( echo. echo -------------------- %%f -------------------- -- cgit v1.2.3