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
|
// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
/*
Rustan Leino, 5 Oct 2011
COST Verification Competition, Challenge 2: Maximum in a tree
http://foveoos2011.cost-ic0701.org/verification-competition
Given: A non-empty binary tree, where every node carries an integer.
Implement and verify a program that computes the maximum of the values
in the tree.
Please base your program on the following data structure signature:
public class Tree {
int value;
Tree left;
Tree right;
}
You may represent empty trees as null references or as you consider
appropriate.
*/
// Remarks:
// The specification of this program uses the common dynamic-frames idiom in Dafny: the
// ghost field 'Contents' stores the abstract value of an object, the ghost field 'Repr'
// stores the set of (references to) objects that make up the representation of the object
// (which in this case is the Tree itself plus the 'Repr' sets of the left and right
// subtrees), and a function 'Valid()' that returns 'true' when an object is in a
// consistent state (that is, when an object satisfies the "class invariant").
// The design I used was to represent an empty tree as a Tree object whose left and
// right pointers point to the object iself. This is convenient, because it lets
// clients of Tree and the implementation of Tree always use non-null pointers to
// Tree objects.
// What needs to be human-trusted about this program is that the 'requires' and
// 'ensures' clauses (that is, the pre- and postconditions, respectively) of
// 'ComputeMax' are correct. And, since the specification talks about the ghost
// variable 'Contents', one also needs to trust that the 'Valid()' function
// constrains 'Contents' in a way that a human thinks matches the intuitive
// definition of what the contents of a tree is.
// To give a taste of that the 'Valid()' function does not over-constrain the
// object, I have included two instance constructors, 'Empty()' and 'Node(...)'.
// To take this a step further, one could also write a 'Main' method that
// builds somme tree and then calls 'ComputeMax', but I didn't do that here.
// About Dafny:
// As always (when it is successful), Dafny verifies that the program does not
// cause any run-time errors (like array index bounds errors), that the program
// terminates, that expressions and functions are well defined, and that all
// specifications are satisfied. The language prevents type errors by being type
// safe, prevents dangling pointers by not having an "address-of" or "deallocate"
// operation (which is accommodated at run time by a garbage collector), and
// prevents arithmetic overflow errors by using mathematical integers (which
// is accommodated at run time by using BigNum's). By proving that programs
// terminate, Dafny proves that a program's time usage is finite, which implies
// that the program's space usage is finite too. However, executing the
// program may fall short of your hopes if you don't have enough time or
// space; that is, the program may run out of space or may fail to terminate in
// your lifetime, because Dafny does not prove that the time or space needed by
// the program matches your execution environment. The only input fed to
// the Dafny verifier/compiler is the program text below; Dafny then automatically
// verifies and compiles the program (for this program in less than 2.5 seconds)
// without further human intervention.
class Tree {
// an empty tree is represented by a Tree object with left==this==right
var value: int;
var left: Tree;
var right: Tree;
ghost var Contents: seq<int>;
ghost var Repr: set<object>;
function Valid(): bool
reads this, Repr;
{
this in Repr &&
left != null && right != null &&
((left == this == right && Contents == []) ||
(left in Repr && left.Repr <= Repr && this !in left.Repr &&
right in Repr && right.Repr <= Repr && this !in right.Repr &&
left.Valid() && right.Valid() &&
Contents == left.Contents + [value] + right.Contents))
}
function method IsEmpty(): bool
requires Valid();
reads this, Repr;
ensures IsEmpty() <==> Contents == [];
{
left == this
}
constructor Empty()
modifies this;
ensures Valid() && Contents == [];
{
left, right := this, this;
Contents := [];
Repr := {this};
}
constructor Node(lft: Tree, val: int, rgt: Tree)
requires lft != null && rgt != null && lft.Valid() && rgt.Valid();
requires this !in lft.Repr && this !in rgt.Repr;
modifies this;
ensures Valid() && Contents == lft.Contents + [val] + rgt.Contents;
{
left, value, right := lft, val, rgt;
Contents := lft.Contents + [val] + rgt.Contents;
Repr := lft.Repr + {this} + rgt.Repr;
}
lemma exists_intro<T>(P: T -> bool, x: T)
requires P.requires(x)
requires P(x)
ensures exists y :: P.requires(y) && P(y) { }
method ComputeMax() returns (mx: int)
requires Valid() && !IsEmpty();
ensures forall x :: x in Contents ==> x <= mx;
ensures exists x :: x in Contents && x == mx;
decreases Repr;
{
mx := value;
if (!left.IsEmpty()) {
var m := left.ComputeMax();
mx := if mx < m then m else mx;
}
if (!right.IsEmpty()) {
var m := right.ComputeMax();
mx := if mx < m then m else mx;
}
exists_intro(x reads this => x in Contents && x == mx, mx);
}
}
|
