why3/stdlib/stack.mlw

(** {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