blob: eb4ff1b9812b0a85177cb1406a436c311f6e7514 (
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
130
|
// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint.dfy" /autoTriggers:0 "%s" > "%t"
// RUN: %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()
|
