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
|
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) {
x1.Down(x0);
}
method WayDown(x0: MyClass0, g: ClassG) {
x0.Down();
g.T(); // allowed, because this follows import relation
var t := g.TFunc(); // allowed, because this follows import relation
}
method Up() {
}
method Somewhere(y: MyClassY) {
y.M(); // error: does not follow import relation
}
}
}
module X1 imports X0 {
class MyClass1 {
method Down(x0: MyClass0) {
x0.Down();
}
method Up(x2: MyClass2) {
x2.Up(); // error: does not follow import relation
}
}
}
module X0 {
class MyClass0 {
method Down() {
}
method Up(x1: MyClass1, x2: MyClass2) {
x1.Up(x2); // error: does not follow import relation
}
}
}
module YY {
class MyClassY {
method M() { }
method P(g: ClassG) {
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) {
y.M(); // error: does not follow import relation
}
}
method Ping() {
Pong(); // allowed: intra-module call
}
method Pong() {
Ping(); // allowed: intra-module call
}
method ProcG(g: ClassG) {
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;
Callee(x, y); // fine
Callee(x, x); // fine
Callee(y, x); // error: cannot pass in ghost to a physical formal
Theorem(x); // fine
Theorem(y); // fine, because it's a ghost method
}
method Callee(a: int, ghost b: int) { }
ghost method Theorem(a: int) { }
}
var SomeField: int;
method SpecialFunctions()
modifies this;
{
SomeField := SomeField + 4;
var a := old(SomeField); // error: old can only be used in ghost contexts
var b := fresh(this); // error: fresh can only be used in ghost contexts
var c := allocated(this); // error: allocated can only be used in ghost contexts
if (fresh(this)) { // this guard makes the if statement a ghost statement
ghost var x := old(SomeField); // this is a ghost context, so it's okay
ghost var y := allocated(this); // this is a ghost context, so it's okay
}
}
// ---------------------- illegal match expressions ---------------
datatype Tree = Nil | Cons(int, Tree, Tree);
function NestedMatch0(tree: Tree): int
{
match tree
case Nil => 0
case Cons(h,l,r) =>
match tree // error: cannot match on "tree" again
case Nil => 0
case Cons(hh,ll,rr) => hh
}
function NestedMatch1(tree: Tree): int
{
match tree
case Nil => 0
case Cons(h,l,r) =>
match l
case Nil => 0
case Cons(h0,l0,r0) =>
match r
case Nil => 0
case Cons(h1,l1,r1) => h + h0 + h1
}
function NestedMatch2(tree: Tree): int
{
match tree
case Nil => 0
case Cons(h,l,r) =>
match l
case Nil => 0
case Cons(h,l0,tree) => // fine to declare another "h" and "tree" here
match r
case Nil => 0
case Cons(h1,l1,r1) => h + h1
}
function NestedMatch3(tree: Tree): int
{
match tree
case Nil => 0
case Cons(h,l,r) =>
match l
case Nil => 0
case Cons(h0,l0,r0) =>
match l // error: cannot match on "l" again
case Nil => 0
case Cons(h1,l1,r1) => h + h0 + h1
}
|
