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
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
|
// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
module A {
datatype Explicit<T(==)> = Nil | Cons(set<T>, Explicit<T>)
datatype Inferred<T> = Nil | Cons(set<T>, Inferred<T>)
class C {
method M<T>(x: Explicit<T>)
method N<T>(x: Inferred<T>)
}
}
module B refines A {
class C {
method M<T>(x: Explicit<T>)
method N<T(==)>(x: Inferred<T>)
}
}
// ----------------------------
module C {
type X(==)
type Y(==)
}
module D refines C {
class X { }
datatype Y = Red | Green | Blue
}
module E refines C {
codatatype X = Next(int, X) // error: X requires equality and codatatypes don't got it
datatype Y = Nil | Something(Z) | More(Y, Y) // error: Y does not support equality
codatatype Z = Red | Green(X) | Blue
}
module F refines C {
datatype X<T> = Nil | Cons(T, X<T>) // error: not allowed to add a type parameter to type X
class Y<T> { } // error: not allowed to add a type parameter to type Y
}
module G refines C {
datatype X = Nil | Next(Z, X) // error: X does not support equality
datatype Y = Nil | Something(Z) | More(Y, Y) // error: Y does not support equality
codatatype Z = Red | Green | Blue
}
// ----------------------------
module H {
datatype Dt<T> = Nil | Cons(T, Dt)
datatype BulkyList<T> = Nothing | Wrapper(T, BulkyListAux)
datatype BulkyListAux<T> = Kons(set<T>, BulkyListAuxAux)
datatype BulkyListAuxAux<T> = GoBack(BulkyList)
codatatype Stream<T> = Next(head: T, tail: Stream<T>)
method M<T(==)>(x: T)
{ }
function method F<T>(x: BulkyList<T>, y: BulkyList<T>): int
{ if x == y then 5 else 7 } // this equality is allowed
function method G<T>(x: Dt<T>, y: Dt<T>): int
{ if x == y then 5 else 7 } // error: the equality is not allowed, because Dt<T> may not support equality
function method G'<T(==)>(x: Dt<T>, y: Dt<T>): int
{ if x == y then 5 else 7 } // fine
method Caller0(b: BulkyList, y: int) {
match (b) {
case Nothing =>
case Wrapper(t, bla) =>
var u;
if (y < 100) { u := t; }
// The following call is allowed, because it will be inferred that
// 'u' is of a type that supports equality
M(u);
}
}
method Caller1(d: Dt) {
match (d) {
case Nil =>
case Cons(t, rest) =>
M(t); // error: t may be of a type that does not support equality
}
}
method Caller2(co: Stream) {
var d := Cons(co, Nil);
Caller1(d); // case in point for the error in Caller1
}
}
// ----------------------------
module Gh {
datatype D = Nil | Cons(head: int, tail: D, ghost x: int)
method M(n: nat, b: bool, d: D, e: D, ghost g: bool)
ensures b ==> d == e; // fine, this is a ghost declaration
{
ghost var g := 0;
var h := 0;
if d == e { // fine, this is a ghost statement
g := g + 1;
} else {
assert !b;
}
if d == e { // error: not allowed to compare D's in a non-ghost context
h := h + 1;
}
if n != 0 {
M(n-1, b, d, e, d==e); // fine
M(n-1, d==e, d, e, false); // error, cannot pass in d==e like we do
}
GM(d==e, d, e); // fine -- we're calling a ghost method
var y0 := F(b, d==e);
var y1 := F(d==e, false); // error
}
function method F(b: bool, ghost g: bool): int { 6 }
ghost method GM(b: bool, d: D, e: D) // all equalities are fine in a ghost method
ensures b ==> d == e;
{
ghost var g := 0;
var h := 0;
if d == e {
g := g + 1;
} else {
assert !b;
}
if d == e {
h := h + 1;
}
}
}
// ------ deeper nesting ------
module Deep {
codatatype Co = Mo(Co) | NoMo
class C<T> { }
method M(a: set<C<Co>>) {
var s: set<C<Co>>;
var t: set<Co>; // error: set element type must support equality
var co: Co;
var d := G(co, NoMo); // error: actual type parameter for Y (namely, Co) does
// not support equality
d := G(t, t) + G(s, s); // fine, because all sets support equality
}
function method G<Y(==)>(y: Y, z: Y): int { if y == z then 5 else 7 }
method P(b: set<Co>) { // error: set element type must be a type with equality
}
ghost method Q(b: set<Co>) { // fine, since this is a ghost method
}
method R(ghost b: set<Co>) { // fine, since this is a ghost parameter
}
datatype Dt<T> = Bucket(T)
datatype Left<T,U> = Bucket(T)
datatype Right<T,U> = Bucket(set<U>) // note, Dafny infers that U should be U(==)
datatype RightExplicit<T,U(==)> = Bucket(set<U>)
type Syn<A,B,C> = Left<C,A>
method W<alpha(==)>()
{
var a: set<Dt<Co>>; // error: Dt<Co> does not support equality
var b: set<Dt<int>>;
var c: set<Left<int,Co>>;
var d: set<Left<Co,int>>; // error: Left<Co,...> does not support equality
var e: set<Right<Co,Co>>; // error: type parameter 1 to Right is required to support equality
ghost var e': set<Right<Co,Co>>; // fine, since this is a ghost field
var e'': set<RightExplicit<Co,Co>>; // error: cannot instantiate argument 1 with Co
var f: set<Syn<Co,Co,int>>;
var g: set<Syn<int,int,Co>>; // error: Syn<int,int,Co> does not support equality
ghost var h: set<Syn<int,int,Co>>; // in a ghost context, it's cool, though
var i; // error: inferred type (set<Co>) uses invalid set-element type
var j: set; // error: ditto
ghost var k: set<Co>; // type allowed here, because it's a ghost
assert i == k || j == k || true; // this infers the types of 'i' and 'j'
}
method StatementsWithVariables(a: set<C<Co>>) {
var s: set<C<Co>>;
var t: set<Co>; // error: bad type
ghost var u: set<Co>;
var c := new ABC;
forall x | x in {t} { // error: bad type for x
c.f := 0;
}
if t == u {
forall x | x in {t} // fine, because this is a ghost statement
ensures true;
{
}
}
}
class ABC { var f: int; }
method Expressions() {
var t: set<Co>; // error: bad type
var b := forall x | x in {t} :: x == x; // error: bad type
var y := var k: set<Co> := t; k <= t; // error: bad type
}
ghost method GhostThings0(t: set<Co>) {
assert forall x | x in {t} :: x == x;
var y := var k: set<Co> := t; k <= t;
assert y;
}
method GhostThings1(ghost t: set<Co>) {
assert forall x | x in {t} :: x == x;
ghost var y := var k: set<Co> := t; k <= t;
assert y;
}
method InferEqualitySupportIsRequired<A>(s: set<A>)
ghost method DontInferEqualitySupportIsRequired<A>(s: set<A>)
method Explicit<A(==)>(s: set<A>)
method TakesABoolean(b: bool)
method AClient(co: Co, ko: Co) {
Explicit({5});
Explicit({co}); // error: bad type
var b := ko in {co}; // error: bad type (argument for the set)
ghost var bg := ko in {co}; // fine, it's a ghost
InferEqualitySupportIsRequired({co}); // error: bad type
DontInferEqualitySupportIsRequired({co});
TakesABoolean(ko in {co}); // error: bad type
var x := multiset([co,ko,co,ko])[ko]; // error: bad type
var m0 := map[5 := ko]; // no prob
var m1 := map[ko := 5]; // error: bad type
}
}
//--------------------------
module UnderspecifiedTypeParameters {
method UP<T>()
function method UG<T>(): int
method Callee<T(==)>()
class TakesParam<U> { }
method MPG()
{
var g := UG(); // error: type parameter underspecified
UP(); // error: type parameter underspecified
}
method M() {
var zs: set; // error: type is underspecified
Callee<(int)>();
Callee<set>(); // error: type is underspecified
Callee<()>();
// The following
Callee<TakesParam>(); // error: type is underspecified
}
}
module EqualitySupportingTypes {
method P<T>()
function method G<T>(): int
class AClass<V(==),Y> {
static function method H<W,X(==)>(): bool
static method Q<A,B(==)>()
}
method Callee<T(==)>()
function method FCallee<T>(): T
datatype Dt = Dt(f: int -> int)
codatatype Stream<T> = Cons(T, Stream)
method M<ArbitraryTypeArg>()
{
Callee<Dt>(); // error: Dt is not an equality-supporting type
Callee<Stream<int>>(); // error: specified type does not support equality
// set<X> is allowed in a non-ghost context only if X is equality supporting.
// Ditto for multiset<X> and map<X,Y>.
var s3x: set<Dt>; // error: this type not allowed in a non-ghost context
var is3x: iset<Dt>; // error: this type not allowed in a non-ghost context
var mast: multiset<ArbitraryTypeArg>; // error: this type not allowed in a non-ghost context
var qt: seq<Stream<int>>; // allowed
var mp0: map<Dt,int>; // error: this type not allowed in a non-ghost context
var mp1: map<int,Dt>; // allowed
var imp0: imap<Dt,int>; // error: this type not allowed in a non-ghost context
var imp1: imap<int,Dt>; // allowed
var S := FCallee<set>(); // this gives s:set<?>
if 4 in S { // this constrains the type further to be s:set<int>
}
var xy: set<set<int>>;
var xz: set<set<Stream<int>>>; // error: set type argument must support equality
Callee<set<Stream<int>>>(); // bogus: a set shouldn't ever be allowed to take a Stream as an argument (this check seems to be missing for explicit type arguments) -- Note: language definition should be changed, because it doesn't make sense for it to talk about a type appearing in a ghost or non-ghost context. Instead, set/iset/multiset/map/imap should always be allowed to take any type argument, but these types may or may not support equality.
var xg := G<set<Stream<int>>>();
var ac0: AClass<int,int>;
var ac1: AClass<Stream<int>,int>; // error: type parameter 0 is required to support equality
var ac2: AClass<int,Stream<int>>;
var xd0 := ac0.H<real,real>();
var xd1 := ac1.H<Stream<real>,real>(); // error (remnant of the fact that the type of ac1 is not allowed)
var xd2 := ac2.H<real,Stream<real>>(); // error: type parameter 1 is required to support equality
var xe0 := ac0.H<real,real>;
var xe1 := ac1.H<Stream<real>,real>; // error (remnant of the fact that the type of ac1 is not allowed)
var xe2 := ac2.H<real,Stream<real>>; // error: type parameter 1 is required to support equality
var xh0 := AClass<int,int>.H<real,real>();
var xh1 := AClass<int,int>.H<Stream<real>,real>();
var xh2 := AClass<int,int>.H<real,Stream<real>>(); // error: type parameter 1 is required to support equality
var xk0 := AClass<real,real>.H<int,int>;
var xk1 := AClass<Stream<real>,real>.H<int,int>; // error: class type param 0 wants an equality-supporting type
var xk2 := AClass<real,Stream<real>>.H<int,int>;
AClass<Stream<int>,int>.Q<real,real>(); // error: class type param 0 wants an equality-supporting type
AClass<int,Stream<int>>.Q<real,real>();
AClass<int,Stream<int>>.Q<Stream<real>,real>();
AClass<int,Stream<int>>.Q<real,Stream<real>>(); // error: method type param 1 wants an equality-supporting type
/*************************** TESTS YET TO COME
var ac8: AClass<real,real>;
var xd8 := (if 5/0 == 3 then ac0 else ac8).H<real,real>(); // error: this should be checked by the verifier
AClass<int,set<Stream<int>>>.Q<real,real>(); // error: cannot utter "set<Stream<int>>" Or is that okay???
AClass<int,int>.Q<set<Stream<real>>,real>(); // error: cannot utter "set<Stream<real>>" Or is that okay???
var xi0 := AClass<int,set<Stream<int>>>.H<real,real>(); // error: cannot utter "set<Stream<int>>" Or is that okay???
var xi1 := AClass<int,int>.H<real,set<Stream<real>>>(); // error: cannot utter "set<Stream<real>>" Or is that okay???
var x, t, s: seq<int -> int>, fii: int -> int;
if s == t {
x := 5; // error: assigning to non-ghost variable in ghost context
}
if fii in s {
x := 4; // error: assigning to non-ghost variable in ghost context
}
if !(fii in s) {
x := 3; // error: assigning to non-ghost variable in ghost context
}
ghost var ghostset: set<Stream<int>> := {}; // fine, since this is ghost
forall u | 0 <= u < 100
ensures var lets: set<Stream<int>> := {}; lets == lets // this is ghost, so the equality requirement doesn't apply
{
}
*********************************************/
}
}
|