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
|
(** {1 Stacks} *)
(** {2 Polymorphic mutable stacks} *)
module Stack
use mach.peano.Peano
use list.List
use list.Length as L
type t 'a = abstract { mutable elts: list 'a }
val create () : t 'a ensures { result.elts = Nil }
val push (x: 'a) (s: t 'a) : unit writes {s}
ensures { s.elts = Cons x (old s.elts) }
exception Empty
val pop (s: t 'a) : 'a writes {s}
ensures { match old s.elts with Nil -> false
| Cons x t -> result = x /\ s.elts = t end }
raises { Empty -> s.elts = old s.elts = Nil }
val top (s: t 'a) : 'a
ensures { match s.elts with Nil -> false
| Cons x _ -> result = x end }
raises { Empty -> s.elts = Nil }
val safe_pop (s: t 'a) : 'a writes {s}
requires { s.elts <> Nil }
ensures { match old s.elts with Nil -> false
| Cons x t -> result = x /\ s.elts = t end }
val safe_top (s: t 'a) : 'a
requires { s.elts <> Nil }
ensures { match s.elts with Nil -> false
| Cons x _ -> result = x end }
val clear (s: t 'a) : unit writes {s} ensures { s.elts = Nil }
val copy (s: t 'a) : t 'a ensures { result = s }
val is_empty (s: t 'a) : bool
ensures { result = True <-> s.elts = Nil }
function length (s: t 'a) : int = L.length s.elts
val length (s: t 'a) : Peano.t
ensures { result = L.length s.elts }
end
|
