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
|
// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
class Example {
method M(n: int)
{
var i := 0;
while (i < n)
{
i := i + 1;
}
}
}
// -----------------------------------
class Fibonacci {
function Fib(n: int): int
{
if n < 2 then n else Fib(n-2) + Fib(n-1)
}
}
// -----------------------------------
class Ackermann {
function F(m: int, n: int): int
{
if m <= 0 then
n + 1
else if n <= 0 then
F(m - 1, 1)
else
F(m - 1, F(m, n - 1))
}
function G(m: int, n: int): int
requires 0 <= m && 0 <= n;
ensures 0 <= G(m, n);
{
if m == 0 then
n + 1
else if n == 0 then
G(m - 1, 1)
else
G(m - 1, G(m, n - 1))
}
function H(m: nat, n: nat): nat
{
if m == 0 then
n + 1
else if n == 0 then
H(m - 1, 1)
else
H(m - 1, H(m, n - 1))
}
method ComputeAck(m: nat, n: nat) returns (r: nat)
{
if (m == 0) {
r := n + 1;
} else if (n == 0) {
r := ComputeAck(m - 1, 1);
} else {
var s := ComputeAck(m, n - 1);
r := ComputeAck(m - 1, s);
}
}
}
// -----------------------------------
class List {
var data: int;
var next: List;
ghost var ListNodes: set<List>;
function IsAcyclic(): bool
reads *;
decreases ListNodes;
{
this in ListNodes &&
(next != null ==>
next.ListNodes <= ListNodes && this !in next.ListNodes &&
next.IsAcyclic())
}
method Singleton(x: int) returns (list: List)
ensures list != null && list.IsAcyclic();
{
list := new List;
list.data := x;
list.next := null;
list.ListNodes := {list};
}
method Prepend(x: int, tail: List) returns (list: List)
requires tail == null || tail.IsAcyclic();
ensures list != null && list.IsAcyclic();
{
list := new List;
list.data := x;
list.next := tail;
list.ListNodes := if tail == null then {list} else {list} + tail.ListNodes;
}
function Sum(): int
requires IsAcyclic();
reads *;
decreases ListNodes;
{
if next == null then data else data + next.Sum()
}
}
|
