blob: 59191ac3a6d4d4a646768e9fe3f89d7508b04f79 (
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
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
|
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];
}
}
assume forall x :: x in s ==> x >= 0;
calc {
0 < |s|;
==> { assert s[0] >= 0; } // OK: well-formed after previous line
s[0] >= 0; // OK: well-formed after previous line
<==> { assert s[0] >= 0; } // OK: well-formed when the previous line is well-formed
s[0] > 0 || s[0] == 0; // OK: well-formed when the previous line is well-formed
}
calc { // same as the last one, but well-formedness is checked in reverse order
s[0] + 1 > 0;
<==>
s[0] >= 0;
<== { assert s[0] >= 0; }
0 < |s|;
}
}
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
}
// calc expression:
function CalcTest3(s: seq<int>): int {
calc < {
0;
{ assume |s| == 5; }
|s|;
}
s[0]
}
// dangling hints:
method CalcTest4(s: seq<int>)
requires forall n | n in s :: n > 0;
{
calc {
1 + 1;
{ assert 1 + 1 == 2; }
}
calc {
2;
{ assert s[0] > 0; } // error: ill-formed hint
}
calc {
|s| > 0;
==> { assert s[0] > 0; } // okay
}
}
|
