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
|
iterator MyIter()
module Mx {
iterator ExampleIterator(k: int) yields (x: int, y: int)
{
var i := k;
while (true) {
if (i % 77 == 0) { yield; }
yield i, -i;
i := i + 1;
}
}
method IteratorUser() {
var iter := new ExampleIterator.ExampleIterator(15);
iter.k := 12; // error: not allowed to assign to iterator's in-parameters
iter.x := 12; // error: not allowed to assign to iterator's yield-parameters
iter.xs := []; // error: not allowed to assign to iterator's yield-history variables
var j := 0;
while (j < 100) {
var more := iter.MoveNext();
if (!more) {
break;
}
print iter.x, iter.y;
j := j + 1;
}
}
static method StaticM(k: nat) returns (m: int)
{
m := k;
}
module Inner {
iterator YetAnother(x: int, y: int, z: int) yields (a: bool, b: bool)
requires true;
}
class Client {
method M() {
var m := StaticM(5);
var it := new ExampleIterator.ExampleIterator(100);
var a, b := Worker(it);
}
method Worker(xi: ExampleIterator) returns (k: int, m: int) {
k, m := xi.k + xi.x, xi.y;
var mr := xi.MoveNext();
if (mr) {
k := xi.x;
} else {
assert k == xi.k + xi.x && m == xi.y;
}
}
method GenericTester(g0: GenericIterator<bool>, g2: GenericIterator)
requires g0.u;
{
g0.t := true; // error: not allowed to assign to .t
g0.u := true; // error: not allowed to assign to .u
var g1 := new GenericIterator.GenericIterator(20);
assert g1.u < 200; // .u is an integer
assert g2.u == 200; // error: the type parameter of g2 is unknown
var h0 := new GenericIteratorResult.GenericIteratorResult();
// so far, the instantiated type of h0 is unknown
var k := h0.t;
assert k < 87;
var h1 := new GenericIteratorResult.GenericIteratorResult();
// so far, the instantiated type of h1 is unknown
if (*) {
var b: bool := h1.t; // this determines h1 to be of type GenericIteratorResult<bool>
} else {
var x: int := h1.t; // error: h1 would have to be a GenericIteratorResult<int>
}
var h2 := new GenericIteratorResult; // error: constructor is not mentioned
var h3 := new GenericIterator.GenericIterator(30);
if (h3.t == h3.u) {
assert !h3.t; // error: type mismatch
}
}
}
iterator GenericIterator<T>(t: T) yields (u: T)
{
while (true) {
yield t;
}
}
iterator GenericIteratorResult<T>() yields (t: T)
{
while (*) { yield; }
}
class AnotherClient {
method StaticM(b: bool) // [sic]
{
}
method Q() {
StaticM(true); // this is supposed to resolve to AnotherClient.StaticM, not _default.StaticM
}
}
}
|
