blob: 3f24212b013426a57d8bd6f98c4d550852688473 (
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
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
|
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)
ensures P(x) ==> -10 <= x;
{
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 -10 <= y; // this much is known of C.P
assert 0 <= 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();
}
}
// ----- regression test -----------------------------------------
abstract module Regression {
module A
{
predicate p(m: map)
lemma m(m: map)
ensures exists m :: p(m);
}
abstract module B
{
import X as A
}
}
|
