blob: 76925e8e1ca98b69732c9d22f5558e1fcd964a34 (
plain)
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
|
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))
}
*/
}
// -----------------------------------
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()
}
}
|
