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
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
|
// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
codatatype Stream<T> = Cons(head: T, tail: Stream)
function Upward(n: int): Stream<int>
{
Cons(n, Upward(n + 1))
}
copredicate Pos(s: Stream<int>)
{
0 < s.head && Pos(s.tail)
}
colemma {:induction false} PosLemma0(n: int)
requires 1 <= n;
ensures Pos(Upward(n));
{
PosLemma0(n + 1); // this completes the proof
}
colemma {:induction false} PosLemma1(n: int)
requires 1 <= n;
ensures Pos(Upward(n));
{
PosLemma1(n + 1);
if (*) {
assert Pos(Upward(n + 1)); // error: cannot conclude this here, because we only have prefix predicates
}
}
colemma {:induction false} Outside_CoLemma_Caller_PosLemma(n: int)
requires 1 <= n;
ensures Pos(Upward(n));
{
assert Upward(n).tail == Upward(n + 1); // follows from one unrolling of the definition of Upward
PosLemma0(n + 1);
assert Pos(Upward(n+1)); // this follows directly from the previous line, because it isn't a recursive call
// ... and it implies the prefix predicate we're supposed to establish
}
method Outside_Method_Caller_PosLemma(n: int)
requires 1 <= n;
ensures Pos(Upward(n)); // this method postcondition follows just fine
{
assert Upward(n).tail == Upward(n + 1); // follows from one unrolling of the definition of Upward
PosLemma0(n + 1);
assert Pos(Upward(n+1)); // this follows directly from the previous line, because it isn't a recursive call
}
copredicate X(s: Stream) // this is equivalent to always returning 'true'
{
X(s)
}
colemma {:induction false} AlwaysLemma_X0(s: Stream)
ensures X(s); // prove that X(s) really is always 'true'
{ // error: this is not the right proof
AlwaysLemma_X0(s.tail);
}
colemma {:induction false} AlwaysLemma_X1(s: Stream)
ensures X(s); // prove that X(s) really is always 'true'
{
AlwaysLemma_X1(s); // this is the right proof
}
colemma {:induction false} AlwaysLemma_X2(s: Stream)
ensures X(s);
{
AlwaysLemma_X2(s);
if (*) {
assert X(s); // error: cannot conclude the full predicate here
}
}
copredicate Y(s: Stream) // this is equivalent to always returning 'true'
{
Y(s.tail)
}
colemma {:induction false} AlwaysLemma_Y0(s: Stream)
ensures Y(s); // prove that Y(s) really is always 'true'
{
AlwaysLemma_Y0(s.tail); // this is a correct proof
}
colemma {:induction false} AlwaysLemma_Y1(s: Stream)
ensures Y(s);
{ // error: this is not the right proof
AlwaysLemma_Y1(s);
}
colemma {:induction false} AlwaysLemma_Y2(s: Stream)
ensures Y(s);
{
AlwaysLemma_Y2(s.tail);
if (*) {
assert Y(s.tail); // error: not provable here
}
}
copredicate Z(s: Stream)
{
false
}
colemma {:induction false} AlwaysLemma_Z(s: Stream)
ensures Z(s); // says, perversely, that Z(s) is always 'true'
{ // error: this had better not lead to a proof
AlwaysLemma_Z(s);
}
function Doubles(n: int): Stream<int>
{
Cons(2*n, Doubles(n + 1))
}
copredicate Even(s: Stream<int>)
{
s.head % 2 == 0 && Even(s.tail)
}
colemma {:induction false} Lemma0(n: int)
ensures Even(Doubles(n));
{
Lemma0(n+1);
}
function UpwardBy2(n: int): Stream<int>
{
Cons(n, UpwardBy2(n + 2))
}
colemma {:induction false} Lemma1(n: int)
ensures Even(UpwardBy2(2*n));
{
Lemma1(n+1);
}
colemma {:induction false} ProveEquality(n: int)
ensures Doubles(n) == UpwardBy2(2*n);
{
ProveEquality(n+1);
}
colemma {:induction false} BadEquality0(n: int)
ensures Doubles(n) == UpwardBy2(n);
{ // error: postcondition does not hold
BadEquality0(n+1);
}
colemma {:induction false} BadEquality1(n: int)
ensures Doubles(n) == UpwardBy2(n+1);
{ // error: postcondition does not hold
BadEquality1(n+1);
}
// test that match statements/expressions get the correct assumption (which wasn't always the case)
codatatype IList<T> = INil | ICons(head: T, tail: IList<T>)
ghost method M(s: IList)
{
match (s) {
case INil =>
assert s == INil;
case ICons(a, b) =>
assert s == ICons(a, b);
}
}
function G(s: IList): int
{
match s
case INil =>
assert s == INil;
0
case ICons(a, b) =>
assert s == ICons(a, b);
0
}
|
