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
|
// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
/*
The well-known Fibonacci function defined in Dafny. The postcondition of
method FibLemma states a property about Fib, and the body of the method is
code that convinces the program verifier that the postcondition does indeed
hold. Thus, effectively, the method states a lemma and its body gives the
proof.
*/
function Fib(n: nat): nat
decreases n;
{ if n < 2 then n else Fib(n-2) + Fib(n-1) }
lemma FibLemma(n: nat)
ensures Fib(n) % 2 == 0 <==> n % 3 == 0;
decreases n;
{
if (n < 2) {
} else {
FibLemma(n-2);
FibLemma(n-1);
}
}
/*
The 'forall' statement has the effect of applying its body simultaneously
to all values of the bound variables---in the first example, to all k
satisfying 0 <= k < n, and in the second example, to all non-negative n.
*/
lemma FibLemma_Alternative(n: nat)
ensures Fib(n) % 2 == 0 <==> n % 3 == 0;
{
forall k | 0 <= k < n {
FibLemma_Alternative(k);
}
}
lemma FibLemma_All()
ensures forall n :: 0 <= n ==> (Fib(n) % 2 == 0 <==> n % 3 == 0);
{
forall n | 0 <= n {
FibLemma(n);
}
}
/*
A standard inductive definition of a generic List type and a function Append
that concatenates two lists. The lemma states that Append is associative,
and its recursive body gives the inductive proof.
We omitted the explicit declaration and uses of the List type parameter in
the signature of the method, since in simple cases like this, Dafny is able
to fill these in automatically.
*/
datatype List<T> = Nil | Cons(head: T, tail: List<T>)
function Append<T>(xs: List<T>, ys: List<T>): List<T>
decreases xs;
{
match xs
case Nil => ys
case Cons(x, rest) => Cons(x, Append(rest, ys))
}
// The {:induction false} attribute disables automatic induction tactic,
// so we can make the proof explicit.
lemma {:induction false} AppendIsAssociative(xs: List, ys: List, zs: List)
ensures Append(Append(xs, ys), zs) == Append(xs, Append(ys, zs));
decreases xs;
{
match (xs) {
case Nil =>
case Cons(x, rest) =>
AppendIsAssociative(rest, ys, zs);
}
}
// Here the proof is fully automatic - the body of the method is empty,
// yet still verifies.
lemma AppendIsAssociative_Auto(xs: List, ys: List, zs: List)
ensures Append(Append(xs, ys), zs) == Append(xs, Append(ys, zs));
{
}
|
