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
|
(**
{1 VerifyThis @ ETAPS 2017 competition
Challenge 4: Tree Buffer}
See https://formal.iti.kit.edu/ulbrich/verifythis2017/
Author: Jean-Christophe Filliâtre (CNRS)
*)
(* default implementation *)
module Spec
use export int.Int
use export list.List
type buf 'a = { h: int; xs: list 'a }
let rec function take (n: int) (l: list 'a) : list 'a =
match l with
| Nil -> Nil
| Cons x xs -> if n = 0 then Nil
else Cons x (take (n-1) xs) end
let function empty (h: int) : buf 'a =
{ h = h; xs = Nil }
let function add (x: 'a) (b: buf 'a) : buf 'a =
{ b with xs = Cons x b.xs }
let function get (b: buf 'a) : list 'a =
take b.h b.xs
(* the following lemma is useful to verify both Caterpillar and
RealTime implementations below *)
use list.Append
use list.Length
let rec lemma take_lemma (l1 l2 l3: list 'a) (n: int)
requires { 0 <= n <= length l1 }
ensures { take n (l1 ++ l2) = take n (l1 ++ l3) }
variant { l1 }
= match l1 with Nil -> ()
| Cons _ ll1 -> if n > 0 then take_lemma ll1 l2 l3 (n-1) end
end
(* task 1 *)
module Caterpillar
use Spec
use list.Append
use list.Length
type cat 'a = {
ch: int;
xs: list 'a;
xs_len: int;
ys: list 'a;
ghost b: buf 'a; (* the model is the default implementation *)
} invariant {
b.h = ch /\
xs_len = length xs < ch /\
forall len. 0 <= len <= ch -> take len (xs ++ ys) = take len b.xs
} by {
ch = 1; xs = Nil; xs_len = 0; ys = Nil; b = empty 1
}
(* for the three operations, the postcondition uses the default
implementation *)
let cat_empty (h: int) : cat 'a
requires { 0 < h }
ensures { result.b = empty h }
= { ch = h; xs = Nil; xs_len = 0; ys = Nil;
b = empty h }
let cat_add (x: 'a) (c: cat 'a) : cat 'a
ensures { result.b = add x c.b }
= if c.xs_len = c.ch - 1 then
{ c with xs = Nil; xs_len = 0; ys = Cons x c.xs;
b = add x c.b }
else
{ c with xs = Cons x c.xs; xs_len = 1 + c.xs_len;
b = add x c.b }
let cat_get (c: cat 'a) : list 'a
ensures { result = get c.b }
= take c.ch (c.xs ++ c.ys)
end
(* task 2 *)
(* important note: Why3 assumes a garbage collector and so it makes
little sense to implement the real time solution in Why3.
Yet I stayed close to the C++ code, with a queue to_delete where
lists are added when discarded and then destroyed progressively
(at most two conses at a time) in process_queue.
The C++ code seems to be missing the insertion into to_delete,
which I added to rt_add; see my comment below.
*)
module RealTime
use Spec
use list.Append
use list.Length
(* For technical reasons, the global queue cannot contain
polymorphic values, to we assume values to be of some
abstract type "elt". Anyway, the C++ code assumes integer
elements. *)
type elt
(* not different from the Caterpillar implementation
replacing 'a with elt everywhere *)
type rt = {
ch: int;
xs: list elt;
xs_len: int;
ys: list elt;
ghost b: buf elt; (* the model is the default implementation *)
} invariant {
b.h = ch /\
xs_len = length xs < ch /\
forall len. 0 <= len <= ch -> take len (xs ++ ys) = take len b.xs
} by {
ch = 1; xs = Nil; xs_len = 0; ys = Nil; b = empty 1
}
(* garbage collection *)
use queue.Queue as Q
(* note: when translating Why3 to OCaml, this module is mapped
to OCaml's Queue module, where push and pop are O(1) *)
val to_delete: Q.t (list elt)
let de_allocate (l: list elt)
= match l with Nil -> () | Cons _ xs -> Q.push xs to_delete end
let process_queue ()
= try
if not (Q.is_empty to_delete) then de_allocate (Q.pop to_delete);
if not (Q.is_empty to_delete) then de_allocate (Q.pop to_delete)
with Q.Empty -> absurd end
(* no difference wrt Caterpillar *)
let rt_empty (h: int) : rt
requires { 0 < h }
ensures { result.b = empty h }
= { ch = h; xs = Nil; xs_len = 0; ys = Nil;
b = empty h }
(* no difference wrt Caterpillar *)
let rt_get (c: rt) : list elt
ensures { result = get c.b }
= take c.ch (c.xs ++ c.ys)
(* this is where we introduce explicit garbage collection
1. process_queue is called first (as in the C++ code)
2. when ys is discarded, it is added to the queue (which
seems to be missing in the C++ code) *)
let rt_add (x: elt) (c: rt) : rt
ensures { result.b = add x c.b }
= process_queue ();
if c.xs_len = c.ch - 1 then begin
Q.push c.ys to_delete;
{ c with xs = Nil; xs_len = 0; ys = Cons x c.xs;
b = add x c.b }
end else
{ c with xs = Cons x c.xs; xs_len = 1 + c.xs_len;
b = add x c.b }
end
|
