blob: ddb23b5bb65ec783856096ff0a52affb513df7f3 (
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
153
154
155
|
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, because we only have prefix predicates
}
}
comethod Outside_CoMethod_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)
}
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); // error: cannot conclude the full predicate here
}
}
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 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);
}
|
