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
184
185
186
187
188
189
190
191
192
193
|
// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
class C {
var n: set<Node>;
method M(v: Stack)
requires v != null;
{
var o: object := v;
assert o !in n; // should be known from the types involved
}
method N(v: Stack)
/* this time without the precondition */
{
var o: object := v;
assert o !in n; // error: v may be null
}
method A0(a: CP<int,C>, b: CP<int,object>)
{
var x: object := a;
var y: object := b;
assert x == y ==> x == null;
}
method A1(a: CP<int,C>)
{
var x: object := a;
assert (forall b: CP<int,Stack> :: x == b ==> b == null); // follows from type antecedents
}
var a2x: set<CP<C,Node>>;
method A2(b: set<CP<Node,C>>)
requires null !in b;
{
var x: set<object> := a2x;
var y: set<object> := b;
assert x * y == {};
}
method A3(b: set<CP<Node,C>>)
/* this time without the precondition */
{
var x: set<object> := a2x;
var y: set<object> := b;
assert x * y <= {null};
}
method A4(b: set<CP<Node,C>>)
/* again, without the precondition */
{
var x: set<object> := a2x;
var y: set<object> := b;
assert x * y == {}; // error
}
method A5()
decreases *;
{
var a := new CP<int,C>;
var b := new CP<int,object>;
while (a != null)
decreases *; // omit loop termination check (in fact, the loop does not terminate)
{
var x: object := a;
var y: object := b;
assert x == y ==> x == null;
a := a; // make 'a' a loop target
}
}
}
class Stack { }
class Node { }
class CP<T,U> {
}
datatype Data = Lemon | Kiwi(int)
function G(d: Data): int
requires d != Data.Lemon;
{
match d
case Lemon => G(d)
case Kiwi(x) => 7
}
// -------- some things about induction ---------------------------------
datatype Tree<T> = Leaf(T) | Branch(Tree<T>, Tree<T>)
class DatatypeInduction<T> {
function LeafCount<G>(tree: Tree<G>): int
{
match tree
case Leaf(t) => 1
case Branch(left, right) => LeafCount(left) + LeafCount(right)
}
method Theorem0(tree: Tree<T>)
ensures 1 <= LeafCount(tree);
{
assert (forall t: Tree<T> :: 1 <= LeafCount(t));
}
// also make sure it works for an instantiated generic datatype
method Theorem1(bt: Tree<bool>, it: Tree<int>)
ensures 1 <= LeafCount(bt);
ensures 1 <= LeafCount(it);
{
assert (forall t: Tree<bool> :: 1 <= LeafCount(t));
assert (forall t: Tree<int> :: 1 <= LeafCount(t));
}
method NotATheorem0(tree: Tree<T>)
ensures LeafCount(tree) % 2 == 1;
{
assert (forall t: Tree<T> :: LeafCount(t) % 2 == 1); // error: fails for Branch case
}
method NotATheorem1(tree: Tree<T>)
ensures 2 <= LeafCount(tree);
{
assert (forall t: Tree<T> :: 2 <= LeafCount(t)); // error: fails for Leaf case
}
function Predicate(): bool
{
(forall t: Tree<T> :: 2 <= LeafCount(t))
}
method NotATheorem2()
{
assert Predicate(); // error (this tests Related Location for induction via a predicate)
}
// ----- here is a test for induction over integers
method IntegerInduction_Succeeds(a: array<int>)
requires a != null;
requires a.Length == 0 || a[0] == 0;
requires forall j :: 1 <= j && j < a.Length ==> a[j] == a[j-1]+2*j-1;
{
// The following assertion can be proved by induction:
assert forall n {:induction} :: 0 <= n && n < a.Length ==> a[n] == n*n;
}
method IntegerInduction_Fails(a: array<int>)
requires a != null;
requires a.Length == 0 || a[0] == 0;
requires forall j :: 1 <= j && j < a.Length ==> a[j] == a[j-1]+2*j-1;
{
// ...but the induction heuristics don't recognize the situation as one where
// applying induction would be profitable:
assert forall n :: 0 <= n && n < a.Length ==> a[n] == n*n; // error reported
}
}
// --- opaque types with type parameters ---
abstract module OpaqueTypesWithParameters {
type P<A>
method M<B>(p: P<B>) returns (q: P<B>)
{
q := p;
var a := new P<int>[500];
}
method DifferentTypes(a: array<P<int>>, b: array<P<bool>>)
requires a != null && b != null;
// If P were a known type, then it would also be known that P<int> and P<bool>
// would be different types, and then the types of 'a' and 'b' would be different,
// which would imply that the following postcondition would hold.
// However, it is NOT necessarily the case that the type parameters of an opaque
// type actually make the opaque type different. For example, see the refinement
// module CaseInPoint below.
ensures a != b; // error
{
}
}
module CaseInPoint refines OpaqueTypesWithParameters {
type P<A> = real // note, the type parameter is not used
method Client() {
var x := new real[100];
DifferentTypes(x, x);
assert false; // this is provable here, since DifferentTypes has a bogus postcondition
}
}
|
