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
|
// The tests in this file are designed to run through the compiler. They contain
// program snippets that are tricky to compile or whose compilation once was buggy.
module OnceBuggy {
datatype MyDt<T> = Nil | Cons(T, MyDt<T>);
method M<U>(x: MyDt<int>)
{
match (x) {
case Cons(head, tail) =>
var y: int := head;
case Nil =>
}
}
}
// --------------------------------------------------
module CoRecursion {
codatatype Stream<T> = More(head: T, rest: Stream);
function method AscendingChain(n: int): Stream<int>
{
More(n, AscendingChain(n+1))
}
datatype List<T> = Nil | Cons(car: T, cdr: List);
function method Prefix(n: nat, s: Stream): List
{
if n == 0 then Nil else
Cons(s.head, Prefix(n-1, s.rest))
}
class Cell { var data: int; }
// When run, the following method should print
// 400
// 320
// 40
// 41
// 42
method Main() {
var m := 17;
var cell := new Cell;
cell.data := 40;
var mr := More(400, More(320, AscendingChain(cell.data)));
m := 30;
cell.data := 60;
var l := Prefix(5, mr);
while (l != Nil)
decreases l;
{
match (l) { case Cons(x,y) => }
print l.car, "\n";
l := l.cdr;
}
}
}
ghost module S {
class C {
var f: int;
method m()
}
}
module T refines S {
class C {
method m() {
print "in T.C.m()";
}
}
}
module A {
module X as S = T;
module Y as S = T;
module Z = T;
static method run() {
var x := new X.C;
x.m();
var y := new Y.C;
y.m();
var z := new Z.C;
z.m();
}
}
method NotMain() {
A.run();
}
ghost module S1 {
module B as S = T;
static method do()
}
module T1 refines S1 {
static method do() {
var x := 3;
}
}
module A1 {
module X as S1 = T1;
static method run() {
X.do();
var x := new X.B.C;
x.m();
}
}
|
