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
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
|
// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
// The tree datatype
datatype Tree = Leaf | Node(Tree, Tree)
// This datatype is used for the result of the build functions.
// These functions either fail or yield a tree. Since we use
// a side-effect free implementation of the helper
// build_rec, it also has to yield the rest of the sequence,
// which still needs to be processed. For function build,
// this part is not used.
datatype Result = Fail | Res(t: Tree, sOut: seq<int>)
// Function toList converts a tree to a sequence.
// We use Dafny's built-in value type sequence rather than
// an imperative implementation to simplify verification.
// The argument d is added to each element of the sequence;
// it is analogous to the argument d in build_rec.
// The postconditions state properties that are needed
// in the completeness proof.
function toList(d: int, t: Tree): seq<int>
ensures toList(d, t) != [] && toList(d, t)[0] >= d
ensures (toList(d, t)[0] == d) == (t == Leaf)
decreases t
{
match t
case Leaf => [d]
case Node(l, r) => toList(d+1, l) + toList(d+1, r)
}
// Function build_rec is a side-effect free implementation
// of the code given in the problem statement.
// The first postcondition is needed to show that the
// termination measure indeed decreases.
// The second postcondition specifies the soundness
// property; converting the resulting tree back into a
// sequence yields exactly that portion of the input
// sequence that has been consumed.
function method build_rec(d: int, s: seq<int>): Result
ensures build_rec(d, s).Res? ==>
|build_rec(d, s).sOut| < |s| &&
build_rec(d, s).sOut == s[|s|-|build_rec(d, s).sOut|..]
ensures build_rec(d, s).Res? ==>
toList(d,build_rec(d, s).t) == s[..|s|-|build_rec(d, s).sOut|]
decreases |s|, (if s==[] then 0 else s[0]-d)
{
if s==[] || s[0] < d then
Fail
else if s[0] == d then
Res(Leaf, s[1..])
else
var left := build_rec(d+1, s);
if left.Fail? then Fail else
var right := build_rec(d+1, left.sOut);
if right.Fail? then Fail else
Res(Node(left.t, right.t), right.sOut)
}
// Function build is a side-effect free implementation
// of the code given in the problem statement.
// The postcondition specifies the soundness property;
// converting the resulting tree back into a
// sequence yields exactly the input sequence.
// Completeness is proved as a lemma, see below.
function method build(s: seq<int>): Result
ensures build(s).Res? ==> toList(0,build(s).t) == s
{
var r := build_rec(0, s);
if r.Res? && r.sOut == [] then r else Fail
}
// This is the main lemma for the
// completeness theorem. If a sequence s starts with a
// valid encoding of a tree t then build_rec yields a
// result (i.e., does not fail) and the rest of the sequence.
// The body of the method proves the lemma by structural
// induction on t. Dafny proves termination (using the
// height of the term t as termination measure), which
// ensures that the induction hypothesis is applied
// correctly (encoded by calls to this lemma).
lemma lemma0(t: Tree, d: int, s: seq<int>)
ensures build_rec(d, toList(d, t) + s).Res? &&
build_rec(d, toList(d, t) + s).sOut == s
{
match(t) {
case Leaf =>
assert toList(d, t) == [d];
case Node(l, r) =>
assert toList(d, t) + s == toList(d+1, l) + (toList(d+1, r) + s);
// the rest follows from (two invocations of) the (automatically applied) induction hypothesis
}
}
// This lemma states the
// completeness property. It is proved by applying the
// main lemma (lemma0). In this lemma, the bound variables
// of the completeness theorem are passed as arguments;
// the following two lemmas replace these arguments
// by quantified variables.
lemma lemma1(t: Tree, s:seq<int>)
requires s == toList(0, t) + []
ensures build(s).Res?
{
lemma0(t, 0, []);
}
// This lemma introduces the existential quantifier in the completeness
// property.
lemma lemma2(s: seq<int>)
ensures (exists t: Tree :: toList(0,t) == s) ==> build(s).Res?
{
forall t | toList(0,t) == s {
lemma1(t, s);
}
}
// This lemma encodes the completeness theorem.
// For each sequence for which there is a corresponding
// tree, function build yields a result different from Fail.
// The body of the method converts the argument of lemma2
// into a universally quantified variable.
lemma completeness()
ensures forall s: seq<int> :: ((exists t: Tree :: toList(0,t) == s) ==> build(s).Res?)
{
forall s {
lemma2(s);
}
}
// This method encodes the first test harness
// given in the problem statement. The local
// assertions are required by the verifier to
// unfold the necessary definitions.
method harness0()
ensures build([1,3,3,2]).Res? &&
build([1,3,3,2]).t == Node(Leaf, Node(Node(Leaf, Leaf), Leaf))
{
}
// This method encodes the second test harness
// given in the problem statement. The local
// assertions are required by the verifier to
// unfold the necessary definitions.
method harness1()
ensures build([1,3,2,2]).Fail?
{
}
|
