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
|
method M(n: nat) {
assert 0 <= n;
}
method Main() {
call M(25);
call M(-25); // error: cannot pass -25 as a nat
}
var f: nat;
method CheckField(x: nat, y: int)
requires 0 <= y;
modifies this;
{
var y: nat := y;
assert 0 <= f;
while (0 < y)
{
f := f + 1;
if (15 < f) {
f := f - 12;
}
y := y - 1;
}
assert 0 <= f;
f := x; // no problem
f := x + 3; // no problem here either
f := x - 3; // error: cannot prove RHS is a nat
}
method Generic<T>(i: int, t0: T, t1: T) returns (r: T) {
if (0 < i) {
var n: nat := 5;
call j := Generic(i-1, n, -4);
assert 0 <= j; // error: the result is an int, not a nat
var q := FenEric(n, -4);
assert 0 <= q; // error: the result is an int, not a nat
}
r := t1;
}
function method FenEric<T>(t0: T, t1: T): T;
datatype Pair<T> { Pr(T, T); }
method K(n: nat, i: int) {
match (Pair.Pr(n, i)) {
case Pr(k, l) =>
assert k == n; // fine: although the type of k is int, we know it's equal to n
assert 0 <= k;
assert 0 <= l; // error: l is an int
}
}
datatype List<T> {
Nil;
Cons(nat, T, List<T>);
}
method MatchIt(list: List<object>) returns (k: nat)
{
match (list) {
case Nil =>
case Cons(n, extra, tail) =>
call w := MatchIt(tail);
assert 0 <= w;
assert 0 <= n; // fine
assert 0 <= n - 10; // error: possible assertion failure
}
var m := Sum(list);
assert 0 <= m;
k := m;
}
class GenEric<T> {
var f: T;
}
function method GE<T>(d: GenEric<T>): bool { true }
method TestGenEric() {
var ge;
if (ge != null) {
var b := GE(ge);
var n: nat := ge.f; // error: the generic instantiation uses int, not nat
}
}
function method Sum(list: List<object>): nat
{
match list
case Nil => 0
case Cons(x, y, tail) => x + Sum(tail)
}
function BadSum(list: List<object>): nat
{
match list
case Nil => 0
case Cons(x, y, tail) => x + BadSum(tail) - 30 // error: may not be a nat
}
function Abs(x: int): nat
{
if 0 <= x then x else -x
}
|
