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
|
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()
{
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
}
}
|
