blob: 0245ef9f10837ea4c83c70675bd4ff9ab810b32c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
|
// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
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 HasBoundedHeight(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
lemma Theorem(n: nat)
ensures HasBoundedHeight(SmallTree(n));
{
Lemma(n);
}
colemma Lemma(n: nat)
ensures LowerThan(SmallTrees(n), n);
{
if 0 < n {
Lemma(n-1);
}
}
|
