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
|
(** Simple queue implemented using a ring buffer
From
Developing Verified Programs with Dafny.
K. Rustan M. Leino. Tutorial notes, ICSE 2013.
For a similar data structure, see vstte12_ring_buffer.mlw
*)
use int.Int
use seq.Seq as S
use array.Array
type t 'a = {
mutable data: array 'a;
mutable m: int;
mutable n: int;
ghost mutable contents: S.seq 'a; (* = data[m..n[ *)
}
invariant { 0 < length data }
invariant { 0 <= m <= n <= length data }
invariant { S.length contents = n - m }
invariant { forall i. 0 <= i < m - n -> S.get contents i = data[m + i] }
by { data = Array.make 1 (any 'a); m = 0; n = 0; contents = S.empty }
let create (x: 'a) : t 'a
ensures { S.(result.contents == empty) }
=
{ data = Array.make 10 x;
m = 0; n = 0;
contents = S.empty; }
let dequeue (q: t 'a) : (_r: 'a)
requires { S.length q.contents > 0 }
writes { q.m, q.contents }
ensures { S.(q.contents == (old q.contents)[1..]) }
=
let r = q.data[q.m] in
q.m <- q.m + 1;
ghost S.(q.contents <- q.contents[1..]);
r
let enqueue (q: t 'a) (x: 'a) : unit
requires { q.n < length q.data }
writes { q.data.elts, q.n, q.contents }
ensures { S.(q.contents == snoc (old q.contents) x) }
=
q.data[q.n] <- x;
q.n <- q.n + 1;
ghost S.(q.contents <- S.snoc q.contents x)
|
