stack.mlw 1.3 KB
Newer Older
1

MARCHE Claude's avatar
MARCHE Claude committed
2 3 4
(** {1 Stacks} *)

(** {2 Polymorphic mutable stacks} *)
5 6 7

module Stack

8
  use mach.peano.Peano
9 10
  use list.List
  use list.Length as L
11

12
  type t 'a = abstract { mutable elts: list 'a }
13

14
  val create () : t 'a ensures { result.elts = Nil }
15

16 17
  val push (x: 'a) (s: t 'a) : unit writes {s}
    ensures { s.elts = Cons x (old s.elts) }
18 19 20

  exception Empty

21 22 23 24
  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 }
25

Andrei Paskevich's avatar
Andrei Paskevich committed
26
  val top (s: t 'a) : 'a
27 28 29
    ensures { match s.elts with Nil -> false
      | Cons x _ -> result = x end }
    raises  { Empty -> s.elts = Nil }
30

31 32 33 34 35
  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 }

Andrei Paskevich's avatar
Andrei Paskevich committed
36
  val safe_top (s: t 'a) : 'a
37 38 39 40
    requires { s.elts <> Nil }
    ensures { match s.elts with Nil -> false
      | Cons x _ -> result = x end }

41
  val clear (s: t 'a) : unit writes {s} ensures { s.elts = Nil }
42

Andrei Paskevich's avatar
Andrei Paskevich committed
43
  val copy (s: t 'a) : t 'a ensures { result = s }
44

Andrei Paskevich's avatar
Andrei Paskevich committed
45
  val is_empty (s: t 'a) : bool
46
    ensures { result = True <-> s.elts = Nil }
47

48
  function length (s: t 'a) : int = L.length s.elts
49

50
  val length (s: t 'a) : Peano.t
51
    ensures { result = L.length s.elts }
52

53
end