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
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
|
// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
function fact6(n: nat): nat
{
fact(n+6)
}
function fact(n: nat): nat
{
if (n==0) then 1 else n*fact(n-1)
}
ghost method compute_fact6()
ensures fact(6)==720;
{
}
ghost method compute_fact6_plus()
ensures fact6(0)==720;
{
}
datatype intlist = IntNil | IntCons(head: int, tail: intlist)
function intsize(l: intlist): nat
{
if (l.IntNil?) then 0 else 1+intsize(l.tail)
}
function intapp(a: intlist, b: intlist): intlist
{
if (a.IntNil?) then b else IntCons(a.head, intapp(a.tail, b))
}
ghost method compute_intappsize()
ensures intsize(intapp(IntCons(1, IntCons(2, IntNil)), IntCons(3, IntCons(4, IntNil))))==4;
{
}
ghost method compute_intsize4()
ensures intsize(IntCons(1, IntCons(2, IntCons(3, IntCons(4, IntNil))))) == 4;
{
}
function cintsize(l: intlist): nat
{
match l
case IntNil => 0
case IntCons(hd, tl) => 1+cintsize(tl)
}
function cintapp(a: intlist, b: intlist): intlist
{
match a
case IntNil => b
case IntCons(hd, tl) => IntCons(hd, cintapp(tl, b))
}
ghost method compute_cintappsize()
ensures cintsize(cintapp(IntCons(1, IntCons(2, IntNil)), IntCons(3, IntCons(4, IntNil))))==4;
{
}
ghost method compute_cintsize4()
ensures cintsize(IntCons(1, IntCons(2, IntCons(3, IntCons(4, IntNil))))) == 4;
{
}
datatype list<A> = Nil | Cons(head: A, tail: list)
function size(l: list): nat
{
if (l.Nil?) then 0 else 1+size(l.tail)
}
function app(a: list, b: list): list
{
if (a.Nil?) then b else Cons(a.head, app(a.tail, b))
}
ghost method compute_size4()
ensures size(Cons(1, Cons(2, Cons(3, Cons(4, Nil))))) == 4;
{
}
ghost method compute_size4_cons()
ensures size(Cons(IntNil, Cons(IntNil, Cons(IntNil, Cons(IntNil, Nil))))) == 4;
{
}
ghost method compute_appsize()
ensures size(app(Cons(1, Cons(2, Nil)), Cons(3, Cons(4, Nil))))==4;
{
}
datatype exp = Plus(e1: exp, e2: exp) | Num(n: int) | Var(x: int)
function interp(env: map<int,int>, e: exp): int
decreases e;
{
if (e.Plus?) then interp(env, e.e1)+interp(env, e.e2)
else if (e.Num?) then e.n
else if (e.Var? && e.x in env) then env[e.x]
else 0
}
ghost method compute_interp1()
ensures interp(map[], Plus(Plus(Num(1), Num(2)), Plus(Num(3), Num(4))))==10;
{
}
ghost method compute_interp2(env: map<int,int>)
requires 0 in env && env[0]==10;
ensures interp(env, Plus(Plus(Var(0), Num(1)), Num(0)))==11;
{
}
ghost method compute_interp3(env: map<int,int>)
requires 0 in env && env[0]==10 && 1 !in env;
ensures interp(env, Plus(Var(0), Plus(Var(1), Var(0))))==20;
{
}
function cinterp(env: map<int,int>, e: exp): int
decreases e;
{
match e
case Plus(e1, e2) => cinterp(env, e1)+cinterp(env, e2)
case Num(n) => n
case Var(x) => if x in env then env[x] else 0
}
ghost method compute_cinterp1()
ensures cinterp(map[], Plus(Plus(Num(1), Num(2)), Plus(Num(3), Num(4))))==10;
{
}
ghost method compute_cinterp2(env: map<int,int>)
requires 0 in env && env[0]==10;
ensures cinterp(env, Plus(Plus(Var(0), Num(1)), Num(0)))==11;
{
}
ghost method compute_cinterp3(env: map<int,int>)
requires 0 in env && env[0]==10 && 1 !in env;
ensures cinterp(env, Plus(Var(0), Plus(Var(1), Var(0))))==20;
{
}
function opt(e: exp): exp
{
match e
case Num(n) => e
case Var(x) => e
case Plus(e1, e2) =>
var o1 := opt(e1);
if (o1.Num? && o1.n==0) then e2 else Plus(o1, e2)
}
ghost method opt_test()
ensures opt(Plus(Plus(Plus(Num(0), Num(0)), Num(0)), Num(1)))==Num(1);
{
}
function copt(e: exp): exp
{
match e
case Num(n) => e
case Var(x) => e
case Plus(e1, e2) => match e1
case Num(n) => if n==0 then e2 else e
case Var(x) => e
case Plus(e11, e12) =>
var o1 := copt(e1);
if (o1.Num? && o1.n==0) then e2 else Plus(o1, e2)
}
ghost method copt_test()
ensures copt(Plus(Plus(Plus(Num(0), Num(0)), Num(0)), Num(1)))==Num(1);
{
}
function power(b: int, n: nat): int
{
if (n==0) then 1 else b*power(b, n-1)
}
ghost method test_power()
ensures power(power(2, 3), 1+power(2, 2))==32768;
{
}
function fib(n: nat): nat
{
if (n<2) then n else fib(n-1)+fib(n-2)
}
ghost method test_fib()
ensures fib(12)==144;
{
}
ghost method test_fib1(k: nat)
ensures k==12 ==> fib(k)==144;
{
}
ghost method test_fib2(k: nat)
ensures 12<=k && k<=12 ==> fib(k)==144;
{
}
ghost method test_fib3(k: nat, m: nat)
{
var y := 12;
assert y <= k && k < y + m && m == 1 ==> fib(k)==144;
}
module NeedsAllLiteralsAxiom {
// The following test shows that there exist an example that
// benefits from the all-literals axiom. (It's not clear how
// important such an example is, nor is it clear what the cost
// of including the all-literals axiom is.)
function trick(n: nat, m: nat): nat
decreases n; // note that m is not included
{
if n < m || m==0 then n else trick(n-m, m) + m
}
lemma lemma_trick(n: nat, m: nat)
ensures trick(n, m) == n;
{
}
lemma calc_trick(n: nat, m: nat)
ensures trick(100, 10) == 100;
{
}
}
|
