blob: c77bced76b41042cf11a2a1f69ba2724798af74b (
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
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
|
// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint.dfy" "%s" > "%t"; %dafny /noVerify /compile:0 "%t.dprint.dfy" >> "%t"
// RUN: %diff "%s.expect" "%t"
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
}
}
// ------------- tests for the pretty printer -------------
lemma CalcPrinting()
{
calc < {
2;
<= { SubLemma(); }
3;
5;
< { assert 5 < 6 <= 5+1; SubLemma(); assert 6 < 7; }
7;
11;
{ SubLemma(); } // dangling hint
}
calc < {
13;
}
calc {
17;
== { SubLemma(); } // dangling hint, following operator
}
calc <= {
19;
<=
{ SubLemma(); }
{ assert 19 + 23 == 42; }
calc { 811; }
{ assert 42 < 100; }
23;
{ calc < {
71; { assert 71 % 19 != 0; } 73;
} }
29;
calc < {
311; 313; 331;
}
31;
}
calc {
}
}
lemma SubLemma()
|
