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
|
datatype List<T> = Nil | Cons(hd: T, tl: List);
method M0() {
var l: List;
l := Cons(5, Nil);
assert l.hd == 5;
var k: MyClass<bool>;
k := new MyClass;
k.data := false;
var h := new MyClass;
h.data := false;
var y := new MyClass.Init(120);
var z: int := y.data;
}
method M1() { // same thing as above, but with types filled in explicitly
var l: List<int>;
l := Cons(5, Nil);
assert l.hd == 5;
var k: MyClass<bool>;
k := new MyClass<bool>;
k.data := false;
var h := new MyClass<bool>;
h.data := false;
var y := new MyClass<int>.Init(120);
var z: int := y.data;
}
class MyClass<G> {
var data: G;
method Init(g: G)
modifies this;
{
data := g;
}
}
// ---------------------------------------------------
// The followinng functions and methods are oblivious of the fact that
// List takes a type parameter.
function concat(xs: List, ys: List): List
{
match xs
case Nil => ys
case Cons(x, tail) => Cons(x, concat(tail, ys))
}
function reverse(xs: List): List
{
match xs
case Nil => Nil
case Cons(t, rest) => concat(reverse(rest), Cons(t, Nil))
}
ghost method Theorem(xs: List)
ensures reverse(reverse(xs)) == xs;
{
match (xs) {
case Nil =>
case Cons(t, rest) =>
Lemma(reverse(rest), Cons(t, Nil));
}
}
ghost method Lemma(xs: List, ys: List)
ensures reverse(concat(xs, ys)) == concat(reverse(ys), reverse(xs));
{
match (xs) {
case Nil =>
assert forall ws :: concat(ws, Nil) == ws;
case Cons(t, rest) =>
assert forall a, b, c :: concat(a, concat(b, c)) == concat(concat(a, b), c);
}
}
// ------ Here are some test cases where the inferred arguments will be a prefix of the given ones
method DoAPrefix<A, B, C>(xs: List) returns (ys: List<A>)
{
ys := xs;
}
function FDoAPrefix<A, B, C>(xs: List): List<A>
{
xs
}
|
