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
|
(** {1 Polymorphic mutable queues}
The module `Queue` below is mapped to OCaml's standard library
module `Queue` by Why3's extraction.
Independently, a Why3 implementation of this module is also
provided in `examples/queue_two_lists.mlw`.
*)
module Queue
use seq.Seq
use mach.peano.Peano
use int.Int
type t 'a = abstract {
mutable seq: Seq.seq 'a;
}
meta coercion function seq
val create () : t 'a
ensures { result = empty }
val push (x: 'a) (q: t 'a) : unit
writes { q }
ensures { q = snoc (old q) x }
exception Empty
val 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 }
val peek (q: t 'a) : 'a
ensures { q <> empty }
ensures { result = q[0] }
raises { Empty -> q = empty }
val safe_pop (q: t 'a) : 'a
requires { q <> empty }
writes { q }
ensures { result = (old q)[0] }
ensures { q = (old q)[1 ..] }
val safe_peek (q: t 'a) : 'a
requires { q <> empty }
ensures { result = q[0] }
val clear (q: t 'a) : unit
writes { q }
ensures { q = empty }
val copy (q: t 'a) : t 'a
ensures { result == q }
val is_empty (q: t 'a) : bool
ensures { result <-> (q = empty) }
val length (q: t 'a) : Peano.t
ensures { result = length q }
val transfer (q1 q2: t 'a) : unit
writes { q1, q2 }
ensures { q1 = empty }
ensures { q2 = (old q2) ++ (old q1) }
end
|
