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
|
class C {
var data: int;
var n: nat;
var st: set<object>;
ghost method CLemma(k: int)
requires k != -23;
ensures data < k; // magic, isn't it (or bogus, some would say)
}
// This method more or less just tests the syntax, resolution, and basic verification
method ParallelStatement_Resolve(
a: array<int>,
spine: set<C>,
Repr: set<object>,
S: set<int>,
clx: C, cly: C, clk: int
)
requires a != null && null !in spine;
modifies a, spine;
{
parallel (i: int | 0 <= i < a.Length && i % 2 == 0) {
a[i] := a[(i + 1) % a.Length] + 3;
}
parallel (o | o in spine) {
o.st := o.st + Repr;
}
parallel (x, y | x in S && 0 <= y+x < 100) {
Lemma(clx, x, y); // error: precondition does not hold (clx may be null)
}
parallel (x, y | x in S && 0 <= y+x < 100) {
cly.CLemma(x + y); // error: receiver might be null
}
parallel (p | 0 <= p)
ensures F(p) <= Sum(p) + p - 1; // error (no connection is known between F and Sum)
{
assert 0 <= G(p);
ghost var t;
if (p % 2 == 0) {
assert G(p) == F(p+2); // error (there's nothing that gives any relation between F and G)
t := p+p;
} else {
assume H(p, 20) < 100; // don't know how to justify this
t := p;
}
PowerLemma(p, t);
t := t + 1;
PowerLemma(p, t);
}
}
method Lemma(c: C, x: int, y: int)
requires c != null;
ensures c.data <= x+y;
ghost method PowerLemma(x: int, y: int)
ensures Pred(x, y);
function F(x: int): int
function G(x: int): nat
function H(x: int, y: int): int
function Sum(x: int): int
function Pred(x: int, y: int): bool
// ---------------------------------------------------------------------
method M0(S: set<C>)
requires null !in S;
modifies S;
ensures forall o :: o in S ==> o.data == 85;
ensures forall o :: o != null && o !in S ==> o.data == old(o.data);
{
parallel (s | s in S) {
s.data := 85;
}
}
method M1(S: set<C>, x: C)
requires null !in S && x in S;
{
parallel (s | s in S)
ensures s.data < 100;
{
assume s.data == 85;
}
if (*) {
assert x.data == 85; // error (cannot be inferred from parallel ensures clause)
} else {
assert x.data < 120;
}
parallel (s | s in S)
ensures s.data < 70; // error
{
assume s.data == 85;
}
}
method M2() returns (a: array<int>)
ensures a != null;
ensures forall i,j :: 0 <= i < a.Length/2 <= j < a.Length ==> a[i] < a[j];
{
a := new int[250];
parallel (i: nat | i < 125) {
a[i] := 423;
}
parallel (i | 125 <= i < 250) {
a[i] := 300 + i;
}
}
method M4(S: set<C>, k: int)
modifies S;
{
parallel (s | s in S && s != null) {
s.n := k; // error: k might be negative
}
}
method M5()
{
if {
case true =>
parallel (x | 0 <= x < 100) {
PowerLemma(x, x);
}
assert Pred(34, 34);
case true =>
parallel (x,y | 0 <= x < 100 && y == x+1) {
PowerLemma(x, y);
}
assert Pred(34, 35);
case true =>
parallel (x,y | 0 <= x < y < 100) {
PowerLemma(x, y);
}
assert Pred(34, 35);
case true =>
parallel (x | x in set k | 0 <= k < 100) {
PowerLemma(x, x);
}
assert Pred(34, 34);
}
}
method Main()
{
var a := new int[180];
parallel (i | 0 <= i < 180) {
a[i] := 2*i + 100;
}
var sq := [0, 0, 0, 2, 2, 2, 5, 5, 5];
parallel (i | 0 <= i < |sq|) {
a[20+i] := sq[i];
}
parallel (t | t in sq) {
a[t] := 1000;
}
parallel (t,u | t in sq && t < 4 && 10 <= u < 10+t) {
a[u] := 6000 + t;
}
var k := 0;
while (k < 180) {
if (k != 0) { print ", "; }
print a[k];
k := k + 1;
}
print "\n";
}
method DuplicateUpdate() {
var a := new int[180];
var sq := [0, 0, 0, 2, 2, 2, 5, 5, 5];
if (*) {
parallel (t,u | t in sq && 10 <= u < 10+t) {
a[u] := 6000 + t; // error: a[10] (and a[11]) are assigned more than once
}
} else {
parallel (t,u | t in sq && t < 4 && 10 <= u < 10+t) {
a[u] := 6000 + t; // with the 't < 4' conjunct in the line above, this is fine
}
}
}
|
