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
133
134
135
136
137
138
139
140
141
|
// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
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(15);
iter.k := 12; // error: not allowed to assign to iterator's in-parameters
iter.x := 12; // allowed (but this destroys the validity of 'iter'
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;
}
}
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(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; // allowed (but this destroys the validity of 'iter'
var g1 := new 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._ctor();
// so far, the instantiated type of h0 is unknown
var k := h0.t;
assert k < 87;
var h1 := new 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._ctor(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
}
}
}
// --------------------------------- _decreases<n> fields
class Cell
{
var data: int;
}
iterator Dieter0(c: Cell)
requires c != null;
decreases c.data, c.data, c != null;
{
assert _decreases0 == _decreases1;
assert _decreases2;
assert _decreases3 == null; // error: there is no _decreases3
assert _decreases0 == null; // error: type mismatch
_decreases2 := false; // error: the field is immutable
}
iterator Dieter1(c: Cell)
requires c != null;
{
assert _decreases0 == c;
assert _decreases1; // error: there is no _decreases1
}
iterator Dieter2()
{
assert _decreases0 == null; // error: there is no _decreases0
}
|
