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
|
(** Implementation of a mutable queue using two lists.
Author: Léo Andrès (Univ. paris-Sud) *)
module Queue
use int.Int
use mach.peano.Peano
use list.List
use list.Length
use list.Reverse
use list.NthNoOpt
use list.Append
use seq.Seq
use seq.FreeMonoid
type t 'a = {
mutable front: list 'a; (* entry *)
mutable rear: list 'a; (* exit *)
ghost mutable seq: Seq.seq 'a;
}
invariant { length seq = Length.length front + Length.length rear }
invariant { Length.length front > 0 -> Length.length rear > 0 }
invariant {
forall i. 0 <= i < length seq ->
seq[i] =
let n = Length.length rear in
if i < n then nth i rear
else nth (Length.length front - 1 - (i - n)) front }
meta coercion function seq
let create () : t 'a
ensures { result = empty }
= {
front = Nil;
rear = Nil;
seq = empty
}
let push (x: 'a) (q: t 'a) : unit
writes { q }
ensures { q = snoc (old q) x }
= match q.front, q.rear with
| Nil, Nil -> q.rear <- Cons x Nil
| _ -> q.front <- Cons x q.front
end;
q.seq <- snoc q.seq x
let rec lemma nth_append (i: int) (l1: list 'a) (l2: list 'a)
requires { 0 <= i < Length.length l1 + Length.length l2 }
ensures {
nth i (Append.(++) l1 l2) =
if i < Length.length l1 then nth i l1
else nth (i - Length.length l1) l2 }
variant { l1 }
=
match l1 with
| Nil -> ()
| Cons _ r1 ->
if i > 0 then nth_append (i - 1) r1 l2
end
(* TODO: move this to stdlib ? *)
let rec lemma nth_rev (i: int) (l: list 'a)
requires { 0 <= i < Length.length l }
ensures { nth i l = nth (Length.length l - 1 - i) (reverse l) }
variant { l }
=
match l with
| Nil -> absurd
| Cons _ s ->
if i > 0 then nth_rev (i - 1) s
end
exception Empty
let pop (q: t 'a) : 'a
writes { q }
ensures { (old q) <> empty }
ensures { result = (old q)[0] }
ensures { q = (old q)[1 ..] }
raises { Empty -> q = old q = empty }
=
let res = match q.rear with
| Nil -> raise Empty
| Cons x Nil -> q.front, q.rear <- Nil, reverse q.front; x
| Cons x s -> q.rear <- s; x
end in
q.seq <- q.seq [1 ..];
res
let peek (q: t 'a) : 'a
ensures { q <> empty }
ensures { result = q[0] }
raises { Empty -> q == empty }
=
match q.rear with
| Nil -> raise Empty
| Cons x _ -> x
end
let safe_pop (q: t 'a) : 'a
requires { q <> empty }
writes { q }
ensures { result = (old q)[0] }
ensures { q = (old q)[1 ..] }
= try pop q with Empty -> absurd end
let safe_peek (q: t 'a) : 'a
requires { q <> empty }
ensures { result = q[0] }
= try peek q with Empty -> absurd end
let clear (q: t 'a) : unit
writes { q }
ensures { q = empty }
=
q.seq <- empty;
q.rear <- Nil;
q.front <- Nil
let copy (q: t 'a) : t 'a
ensures { result == q }
= {
front = q.front;
rear = q.rear;
seq = q.seq
}
let is_empty (q: t 'a)
ensures { result <-> q == empty }
=
match q.front, q.rear with
| Nil, Nil -> true
| _ -> false
end
let length (q: t 'a) : Peano.t
ensures { result = Seq.length q.seq }
=
let rec length_aux (acc: Peano.t) (l: list 'a) : Peano.t
ensures { result = acc + Length.length l }
variant { l }
= match l with
| Nil -> acc
| Cons _ s -> length_aux (Peano.succ acc) s
end in
length_aux (length_aux Peano.zero q.front) q.rear
let transfer (q1: t 'a) (q2: t 'a) : unit
writes { q1, q2 }
ensures { q1 = empty }
ensures { q2 = (old q2) ++ (old q1) }
= match q2.rear with
| Nil ->
q2.front, q2.rear, q2.seq <- q1.front, q1.rear, q1.seq
| _ ->
q2.front <- Append.(++) q1.front (Append.(++) (reverse q1.rear) q2.front);
q2.seq <- q2.seq ++ q1.seq;
end;
clear q1
end
(** the module above is a valid implementation of queue.Queue *)
module Correct
use Queue as Q
clone queue.Queue with
type t = Q.t, exception Empty = Q.Empty,
val create = Q.create, val push = Q.push, val pop = Q.pop, val peek = Q.peek,
val safe_pop = Q.safe_pop, val safe_peek = Q.safe_peek,
val clear = Q.clear, val copy = Q.copy, val is_empty = Q.is_empty,
val length = Q.length, val transfer = Q.transfer
end
|
