blob: c555bc99bc795eb889659c04040ac86ce095dacc (
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
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
|
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)
}
comethod PosLemma0(n: int)
requires 1 <= n;
ensures Pos(Upward(n));
{
PosLemma0(n + 1); // this completes the proof
}
comethod PosLemma1(n: int)
requires 1 <= n;
ensures Pos(Upward(n));
{
PosLemma1(n + 1);
if (*) {
assert Pos(Upward(n + 1)); // error: cannot conclude this here
}
}
comethod OutsideCaller_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, but it's not a recursive call
}
copredicate X(s: Stream) // this is equivalent to always returning 'true'
{
X(s)
}
comethod 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);
}
comethod AlwaysLemma_X1(s: Stream)
ensures X(s); // prove that X(s) really is always 'true'
{
AlwaysLemma_X1(s); // this is the right proof
}
comethod AlwaysLemma_X2(s: Stream)
ensures X(s);
{
AlwaysLemma_X2(s);
if (*) {
assert X(s); // actually, we can conclude this here, because the X(s) we're trying to prove gets expanded
}
}
copredicate Y(s: Stream) // this is equivalent to always returning 'true'
{
Y(s.tail)
}
comethod AlwaysLemma_Y0(s: Stream)
ensures Y(s); // prove that Y(s) really is always 'true'
{
AlwaysLemma_Y0(s.tail); // this is a correct proof
}
comethod AlwaysLemma_Y1(s: Stream)
ensures Y(s);
{ // error: this is not the right proof
AlwaysLemma_Y1(s);
}
comethod 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
}
comethod 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)
}
comethod Lemma0(n: int)
ensures Even(Doubles(n));
{
Lemma0(n+1);
}
function UpwardBy2(n: int): Stream<int>
{
Cons(n, UpwardBy2(n + 2))
}
comethod Lemma1(n: int)
ensures Even(UpwardBy2(2*n));
{
Lemma1(n+1);
}
comethod BadTheorem(s: Stream<int>)
//TODO: ensures false;
{ // error: cannot establish postcondition 'false', despite the recursive call (this works because CoCall's drop all positive formulas except certificate-based ones)
BadTheorem(s.tail);
}
comethod ProveEquality(n: int)
ensures Doubles(n) == UpwardBy2(2*n);
{
ProveEquality(n+1);
}
comethod BadEquality0(n: int)
ensures Doubles(n) == UpwardBy2(n); // error: postcondition does not hold
{
BadEquality0(n+1);
}
comethod BadEquality1(n: int)
ensures Doubles(n) == UpwardBy2(n+1); // error: postcondition does not hold
{
BadEquality1(n+1);
}
|
