blob: 8b2ff570aebb2fb4baeea43cc981d4173dcfec18 (
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
|
// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
module A {
class C {
var f: int;
}
datatype D = E(int) | F(int);
static function f(n:nat): nat
}
module B {
class C {
var f: int;
}
datatype D = E(int) | F(int);
static function f(n:nat): nat
}
module Test {
import opened A; // nice shorthand for import opened A = A; (see below)
method m() {
var c := new C; // fine, as A was opened
var c' := new A.C;// also fine, as A is bound
var i := 43;
var d := E(i); // these all refer to the same value
var d' := A.E(i);
var d'':= A.D.E(i);
assert d == d' == d'';
assert f(3) >= 0; // true because f(x): nat
assert A._default.f(3) >= 0;
}
}
module Test2 {
import opened B as A;
method m() {
var c := new C; // fine, as A was opened
var c' := new B.C;// also fine, as A is bound
assert B.f(0) >= 0;
}
}
module Test3 {
import opened A;
import opened B; // everything in B clashes with A
method m() {
var c := new C; // bad, ambiguous between A.C and B.C
var c' := new A.C; // good: qualified.
var i := 43;
var d := E(i); // bad, as both A and B give a definition of E
var d' := D.E(i); // bad, as D is still itself ambiguous.
var d'':= B.D.E(i); // good, just use the B version
assert f(3) >= 0; // bad because A and be both define f statically.
}
}
module Test4 {
import A = A; // good: looks strange, but A is not bound on the RHS of the equality
import B; // the same as the above, but for module B
}
|
