blob: 39361b7bf693aed135f281db62c4db5217d8cca4 (
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
91
92
93
94
95
96
97
|
class Termination {
method A(N: int)
requires 0 <= N;
{
var i := 0;
while (i < N)
invariant i <= N;
decreases N - i;
{
i := i + 1;
}
}
method B(N: int)
requires 0 <= N;
{
var i := N;
while (true)
invariant 0 <= i;
decreases i;
{
i := i - 1;
if (!(0 <= i)) {
break;
}
}
assert i == -1;
}
method Lex() {
call x := Update();
call y := Update();
while (!(x == 0 && y == 0))
invariant 0 <= x && 0 <= y;
decreases x, y;
{
if (0 < y) {
y := y - 1;
} else {
x := x - 1;
call y := Update();
}
}
}
method Update() returns (r: int)
ensures 0 <= r;
{
r := 8;
}
method M() {
var b := true;
var i := 500;
var r := new Termination;
var s := {12, 200};
var q := [5, 8, 13];
while (true)
decreases b, i, r;
// invariant b ==> 0 <= i;
decreases s, q;
{
if (12 in s) {
s := s - {12};
} else if (b) {
b := !b;
i := i + 1;
} else if (20 <= i) {
i := i - 20;
} else if (r != null) {
r := null;
} else if (|q| != 0) {
q := q[1..];
} else {
break;
}
}
}
method Q<T>(list: List<T>) {
var l := list;
while (l != #List.Nil)
decreases l;
{
call x, l := Traverse(l);
}
}
method Traverse<T>(a: List<T>) returns (val: T, b: List<T>);
requires a != #List.Nil;
ensures a == #List.Cons(val, b);
}
datatype List<T> {
Nil;
Cons(T, List<T>);
}
|
