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
|
module M {
class T { }
class U { }
}
module N {
class T { } // error: duplicate class name
}
module U imports N { // fine, despite the fact that a class is called U--module names are in their own name space
}
module V imports T { // error: T is not a module
}
module A imports B, M {
class Y { }
}
module B imports N, M {
class X { }
}
module G imports A, M, A, H, B { // error: cycle in import graph
}
module H imports A, N, I {
}
module I imports J {
}
module J imports G, M {
}
// --------------- calls
module X2 imports X1 {
class MyClass2 {
method Down(x1: MyClass1, x0: MyClass0) {
call x1.Down(x0);
}
method WayDown(x0: MyClass0, g: ClassG) {
call x0.Down();
call g.T(); // allowed, because this follows import relation
var t := g.TFunc(); // allowed, because this follows import relation
}
method Up() {
}
method Somewhere(y: MyClassY) {
call y.M(); // error: does not follow import relation
}
}
}
module X1 imports X0 {
class MyClass1 {
method Down(x0: MyClass0) {
call x0.Down();
}
method Up(x2: MyClass2) {
call x2.Up(); // error: does not follow import relation
}
}
}
module X0 {
class MyClass0 {
method Down() {
}
method Up(x1: MyClass1, x2: MyClass2) {
call x1.Up(x2); // error: does not follow import relation
}
}
}
module YY {
class MyClassY {
method M() { }
method P(g: ClassG) {
call g.T(); // allowed, because this follows import relation
var t := g.TFunc(); // allowed, because this follows import relation
}
}
}
class ClassG {
method T() { }
function method TFunc(): int { 10 }
method V(y: MyClassY) {
call y.M(); // error: does not follow import relation
}
}
method Ping() {
call Pong(); // allowed: intra-module call
}
method Pong() {
call Ping(); // allowed: intra-module call
}
method ProcG(g: ClassG) {
call g.T(); // allowed: intra-module call
var t := g.TFunc(); // allowed: intra-module call
}
// ---------------------- some ghost stuff ------------------------
class Ghosty {
method Caller() {
var x := 3;
ghost var y := 3;
call Callee(x, y); // fine
call Callee(x, x); // fine
call Callee(y, x); // error: cannot pass in ghost to a physical formal
call Theorem(x); // fine
call Theorem(y); // fine, because it's a ghost method
}
method Callee(a: int, ghost b: int) { }
ghost method Theorem(a: int) { }
}
|
