Why3 Standard Library index



Polymorphic mutable queues

module Queue

  use import list.List
  use import list.Append
  use import list.Length as L

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

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

  val push (x: 'a) (q: t 'a) : unit writes {q}
    ensures { q.elts = old q.elts ++ Cons x Nil }

  exception Empty

  val pop (q: t 'a) : 'a writes {q}
    ensures { match old q.elts with Nil -> false
      | Cons x t -> result = x /\ q.elts = t end }
    raises  { Empty -> q.elts = old q.elts = Nil }

  val peek (q: t 'a) : 'a
    ensures { match q.elts with Nil -> false
      | Cons x _ -> result = x end }
    raises  { Empty -> q.elts = Nil }

  val safe_pop (q: t 'a) : 'a writes {q}
    requires { q.elts <> Nil }
    ensures { match old q.elts with Nil -> false
      | Cons x t -> result = x /\ q.elts = t end }

  val safe_peek (q: t 'a) : 'a
    requires { q.elts <> Nil }
    ensures { match q.elts with Nil -> false
      | Cons x _ -> result = x end }

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

  val copy (q: t 'a) : t 'a ensures { result = q }

  val is_empty (q: t 'a) : bool
    ensures { result = True <-> q.elts = Nil }

  function length (q: t 'a) : int = L.length q.elts

  val length (q: t 'a) : int
    ensures { result = L.length q.elts }

  val transfer (q1 q2: t 'a) : unit
    writes  { q1, q2 }
    ensures { q1.elts = Nil }
    ensures { q2.elts = old q2.elts ++ old q1.elts }

end


Generated by why3doc 0.87.3