stdlib/stack.mlw

   1
   2 (** {1 Stacks} *)
   3
   4 (** {2 Polymorphic mutable stacks} *)
   5
   6 module Stack
   7
   8   use mach.peano.Peano
   9   use list.List
  10   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   val push (x: 'a) (s: t 'a) : unit writes {s}
  17     ensures { s.elts = Cons x (old s.elts) }
  18
  19   exception Empty
  20
  21   val pop (s: t 'a) : 'a writes {s}
  22     ensures { match old s.elts with Nil -> false
  23       | Cons x t -> result = x /\ s.elts = t end }
  24     raises  { Empty -> s.elts = old s.elts = Nil }
  25
  26   val top (s: t 'a) : 'a
  27     ensures { match s.elts with Nil -> false
  28       | Cons x _ -> result = x end }
  29     raises  { Empty -> s.elts = Nil }
  30
  31   val safe_pop (s: t 'a) : 'a writes {s}
  32     requires { s.elts <> Nil }
  33     ensures { match old s.elts with Nil -> false
  34       | Cons x t -> result = x /\ s.elts = t end }
  35
  36   val safe_top (s: t 'a) : 'a
  37     requires { s.elts <> Nil }
  38     ensures { match s.elts with Nil -> false
  39       | Cons x _ -> result = x end }
  40
  41   val clear (s: t 'a) : unit writes {s} ensures { s.elts = Nil }
  42
  43   val copy (s: t 'a) : t 'a ensures { result = s }
  44
  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