blob: 1f47f3b108aef6b3037e16c4f1c628e95918b204 (
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
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
|
module A {
import B = Babble;
class X {
function Fx(z: B.Z): int
requires z != null;
decreases 5, 4, 3;
{ z.G() } // fine; this goes to a different module
}
datatype Y = Cons(int, Y) | Empty;
}
class C {
method M() { }
function F(): int { 818 }
}
method MyMethod() { }
var MyField: int;
module Babble {
class Z {
method K() { }
function G(): int
decreases 10, 8, 6;
{ 25 }
}
}
static function MyFunction(): int { 5 }
class D { }
method Proc0(x: int)
decreases x;
{
if (0 <= x) {
Proc1(x - 1);
}
}
method Proc1(x: int)
decreases x;
{
if (0 <= x) {
Proc0(x - 1);
}
}
method Botch0(x: int)
decreases x;
{
Botch1(x - 1); // error: failure to keep termination metric bounded
}
method Botch1(x: int)
decreases x;
{
Botch0(x); // error: failure to decrease termination metric
}
// ------ modules ------------------------------------------------
module A_Visibility {
class C {
static predicate P(x: int)
{
0 <= x
}
}
method Main() {
var y;
if (C.P(y)) {
assert 0 <= y; // this much is known of C.P
assert 2 <= y; // error
} else {
assert C.P(8); // this is fine
}
}
}
module B_Visibility {
import A = A_Visibility;
method Main() {
var y;
if (A.C.P(y)) {
assert 0 <= y; // this much is known of C.P
assert 2 <= y; // error
} else {
assert A.C.P(8); // error: C.P cannot be established outside the declaring module
}
}
}
// ------ qualified type names ----------------------------------
module Q_Imp {
class Node { }
class Klassy {
method Init()
}
}
module Q_M {
import Q = Q_Imp;
method MyMethod(root: Q.Node, S: set<Q.Node>)
requires root in S;
{
var i := new Q.Node;
var j := new Q.Node;
assert i != j; // fine
var q := new Q.Klassy.Init();
}
}
|
