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) }
ghost method 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.
*/
ghost method FibLemma_Alternative(n: nat)
ensures Fib(n) % 2 == 0 <==> n % 3 == 0;
{
forall k | 0 <= k < n {
FibLemma_Alternative(k);
}
}
ghost method 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 ghost method states the lemma 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.
ghost method {: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.
ghost method AppendIsAssociative_Auto(xs: List, ys: List, zs: List)
ensures Append(Append(xs, ys), zs) == Append(xs, Append(ys, zs));
{
}
|
