blob: 9e44f62ea8729f53fe3efbbd4fce93bc54e641a8 (
plain)
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
|
method CalcTest0(s: seq<int>) {
calc {
s[0]; // error: ill-formed line
}
calc {
2;
{ assert s[0] == 1; } // error: ill-formed hint
1 + 1;
}
if (|s| > 0) {
calc {
s[0]; // OK: well-formed in this context
{ assert s[0] == s[0]; }
<= s[0];
}
}
}
method CalcTest1(x: int, y: int) {
calc {
x + y;
{ assume x == 0; }
y;
}
assert x == 0; // OK: follows from x + y == y;
}
method CalcTest2(x: int, y: int) {
calc {
x + y;
{ assume x == 0; }
y + x;
}
assert x == 0; // error: even though assumed above, is not exported by the calculation
}
|
