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
|
// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
class C {
function F(c: C, d: D): bool { true }
method M(x: int) returns (y: int, c: C)
requires F(D.A, this); // 2 errors
requires F(4, 5); // 2 errors
requires F(this, D.A); // good
{ }
method Caller()
{
var m,n := M(true); // error on in-parameter
n,m := M(m); // 2 errors on out-parameters
}
}
datatype D = A;
datatype NeverendingList = Cons(int, NeverendingList); // error: no grounding constructor
datatype MutuallyRecursiveDataType<T> =
FromANumber(int) | // this is the base case
Else(TheCounterpart<T>, C);
datatype TheCounterpart<T> =
TreeLike(TheCounterpart<T>, TheCounterpart<T>) |
More(MutuallyRecursiveDataType<T>);
// these 'ReverseOrder_' order tests may be called white-box unit tests
datatype ReverseOrder_MutuallyRecursiveDataType<T> =
FromANumber(int) | // this is the base case
Else(ReverseOrder_TheCounterpart<T>, C);
datatype ReverseOrder_TheCounterpart<T> =
TreeLike(ReverseOrder_TheCounterpart<T>, ReverseOrder_TheCounterpart<T>) |
More(ReverseOrder_MutuallyRecursiveDataType<T>);
// ---------------------
class ArrayTests {
ghost method G(a: array<int>)
requires a != null && 10 <= a.Length;
modifies a;
{
a[7] := 13; // error: array elements are not ghost locations
}
}
// ---------------------
method DuplicateVarName(x: int) returns (y: int)
{
var z: int;
var z: int; // error: redeclaration of local
var x := x; // redeclaration of in-parameter is fine
var x := x; // error: but a redeclaration of that local is not fine
{
var x := x; // an inner local variable of the same name is fine
var x := x; // error: but a redeclaration thereof is not okay
var y := y; // duplicating an out-parameter here is fine
}
var y := y; // error: redeclaration of an out-parameter is not allowed (it is
// treated like an outermost-scoped local in this regard)
}
method ScopeTests()
{
var x := x; // error: the 'x' in the RHS is not in scope
var y :| y == y; // fine, 'y' is in scope in the RHS
var z := DuplicateVarName(z); // error: the 'z' in the RHS is not in scope
var w0, w1 := IntTransform(w1), IntTransform(w0); // errors two
var c := new MyClass.Init(null); // fine
var d := new MyClass.Init(c); // fine
var e := new MyClass.Init(e); // error: the 'e' in the RHS is not in scope
e := new MyClass.Init(e); // fine (no variable is being introduced here)
e.c := new MyClass.Init(e); // also fine
}
function IntTransform(w: int): int
class MyClass {
var c: MyClass;
constructor Init(c: MyClass)
}
// ---------------------
method InitCalls() {
var c := new C.F(null, null); // error: F is not a method
var d := new C.M(8); // error: M has out parameters
var e := new C.Caller();
}
// ---------------------
method ArrayRangeAssignments(a: array<C>, c: C)
requires a != null && 10 <= a.Length;
{
a[0..5] := new C; // error: this is not allowed
a[1..4] := *; // error: this is not allowed
a[2..3] := c; // error: this is not allowed
var s: seq<C> := [null,null,null,null,null];
s[0..5] := new C; // error: this is not allowed
s[1..4] := *; // error: this is not allowed
s[2..3] := c; // error: this is not allowed
}
// --------------------- tests of restrictions on subranges (nat)
method K() {
var s: set<nat>; // error: not allowed to instantiate 'set' with 'nat'
var d: MutuallyRecursiveDataType<nat>; // error: not allowed to instantiate with 'nat'
var a := new nat[100]; // error: not allowed the type array<nat>
var b := new nat[100,200]; // error: not allowed the type array2<nat>
}
// --------------------- more ghost tests, for assign-such-that statements
method M()
{
ghost var b: bool;
ghost var k: int, l: int;
var m: int;
k :| k < 10;
k, m :| 0 <= k < m; // error: LHS has non-ghost and RHS has ghost
m :| m < 10;
// Because of the ghost guard, these 'if' statements are ghost contexts, so only
// assignments to ghosts are allowed.
if (b) {
k :| k < 10; // should be allowed
k, l :| 0 <= k < l; // ditto
}
if (b) {
m :| m < 10; // error: not allowed in ghost context
k, m :| 0 <= k < m; // error: not allowed in ghost context
}
}
ghost method GhostM() returns (x: int)
{
x :| true; // no problem (but there once was a problem with this case, where an error was generated for no reason)
}
|
