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
|
class IntegerInduction {
// This class considers different ways of proving, for any natural n:
// (SUM i in [0, n] :: i^3) == (SUM i in [0, n] :: i)^2
// In terms of Dafny functions, the theorem to be proved is:
// SumOfCubes(n) == Gauss(n) * Gauss(n)
function SumOfCubes(n: int): int
requires 0 <= n;
{
if n == 0 then 0 else SumOfCubes(n-1) + n*n*n
}
function Gauss(n: int): int
requires 0 <= n;
{
if n == 0 then 0 else Gauss(n-1) + n
}
// Here is one proof. It uses a lemma, which is proved separately.
ghost method Theorem0(n: int)
requires 0 <= n;
ensures SumOfCubes(n) == Gauss(n) * Gauss(n);
{
if (n != 0) {
call Theorem0(n-1);
call Lemma(n-1);
}
}
ghost method Lemma(n: int)
requires 0 <= n;
ensures 2 * Gauss(n) == n*(n+1);
{
if (n != 0) { call Lemma(n-1); }
}
// Here is another proof. It states the lemma as part of the theorem, and
// thus proves the two together.
ghost method Theorem1(n: int)
requires 0 <= n;
ensures SumOfCubes(n) == Gauss(n) * Gauss(n);
ensures 2 * Gauss(n) == n*(n+1);
{
if (n != 0) {
call Theorem1(n-1);
}
}
// Here is another proof. It makes use of Dafny's induction heuristics to
// prove the lemma.
ghost method Theorem2(n: int)
requires 0 <= n;
ensures SumOfCubes(n) == Gauss(n) * Gauss(n);
{
if (n != 0) {
call Theorem0(n-1);
assert (forall m :: 0 <= m ==> 2 * Gauss(m) == m*(m+1));
}
}
ghost method M(n: int)
requires 0 <= n;
{
assume (forall k :: 0 <= k && k < n ==> 2 * Gauss(k) == k*(k+1)); // manually assume the induction hypothesis
assert 2 * Gauss(n) == n*(n+1);
}
// Another way to prove the lemma is to supply a postcondition on the Gauss function
ghost method Theorem3(n: int)
requires 0 <= n;
ensures SumOfCubes(n) == GaussWithPost(n) * GaussWithPost(n);
{
if (n != 0) {
call Theorem3(n-1);
}
}
function GaussWithPost(n: int): int
requires 0 <= n;
ensures 2 * GaussWithPost(n) == n*(n+1);
{
if n == 0 then 0 else GaussWithPost(n-1) + n
}
// Finally, with the postcondition of GaussWithPost, one can prove the entire theorem by induction
ghost method Theorem4()
ensures (forall n :: 0 <= n ==> SumOfCubes(n) == GaussWithPost(n) * GaussWithPost(n));
{
// look ma, no hints!
}
ghost method Theorem5(n: int)
requires 0 <= n;
ensures SumOfCubes(n) == GaussWithPost(n) * GaussWithPost(n);
{
// the postcondition is a simple consequence of these quantified versions of the theorem:
if (*) {
assert (forall m :: 0 <= m ==> SumOfCubes(m) == GaussWithPost(m) * GaussWithPost(m));
} else {
call Theorem4();
}
}
// The body of this function method gives a single quantifier, which leads to an efficient
// way to check sortedness at run time. However, an alternative, and ostensibly more general,
// way to express sortedness is given in the function's postcondition. The alternative
// formulation may be easier to understand for a human and may also be more readily applicable
// for the program verifier. Dafny will show that postcondition holds, which ensures the
// equivalence of the two formulations.
// The proof of the postcondition requires induction. It would have been nicer to state it
// as one formula of the form "IsSorted(s) <==> ...", but then Dafny would never consider the
// possibility of applying induction. Instead, the "==>" and "<==" cases are given separately.
// Proving the "<==" case is simple; it's the "==>" case that requires induction.
// The example uses an attribute that requests induction on just "j". However, the proof also
// goes through by applying induction on both bound variables.
function method IsSorted(s: seq<int>): bool
ensures IsSorted(s) ==> (forall i,j {:induction j} :: 0 <= i && i < j && j < |s| ==> s[i] <= s[j]);
ensures (forall i,j :: 0 <= i && i < j && j < |s| ==> s[i] <= s[j]) ==> IsSorted(s);
{
(forall i :: 1 <= i && i < |s| ==> s[i-1] <= s[i])
}
}
datatype Tree<T> {
Leaf(T);
Branch(Tree<T>, Tree<T>);
}
class DatatypeInduction<T> {
function LeafCount<T>(tree: Tree<T>): int
{
match tree
case Leaf(t) => 1
case Branch(left, right) => LeafCount(left) + LeafCount(right)
}
method Theorem0(tree: Tree<T>)
ensures 1 <= LeafCount(tree);
{
assert (forall t: Tree<T> :: 1 <= LeafCount(t));
}
// see also Test/dafny0/DTypes.dfy for more variations of this example
}
|
