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
|
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);
}
}
|
