stack.mlw 1.28 KB
Newer Older
1

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

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

module Stack

  use import list.List
9
  use import list.Length as L
10

11
  type t 'a model { mutable elts: list 'a }
12

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

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

  exception Empty

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

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

30 31 32 33 34
  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
35
  val safe_top (s: t 'a) : 'a
36 37 38 39
    requires { s.elts <> Nil }
    ensures { match s.elts with Nil -> false
      | Cons x _ -> result = x end }

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

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

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
49
  val length (s: t 'a) : int
50
    ensures { result = L.length s.elts }
51

52
end