Why3 Standard Library index



Priority queues


Polymorphic mutable priority queues

module Pqueue

Types

  type elt

the abstract type of elements

  clone export relations.TotalOrder with type t = elt

elt is equipped with a total order rel

  use import list.List
  use import list.Mem
  use import list.Permut
  use import list.Length

  type t model { mutable elts: list elt }

the priority queue is modeled as a list of elements


Operations

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

create a fresh, empty queue

  val push (x: elt) (q: t) : unit writes {q}
    ensures { q.elts = Cons x (old q.elts) }

push an element in a queue

  exception Empty

exception raised by pop and peek to signal an empty queue

  predicate minimal_elt (x: elt) (s: list elt) =
     mem x s /\ forall e: elt. mem e s -> rel x e

property of the element returned by pop and peek

  val pop (q: t) : elt writes {q}
    ensures { permut (Cons result q.elts) (old q.elts) }
    ensures { minimal_elt result (old q.elts) }
    raises  { Empty -> q.elts = (old q.elts) = Nil }

remove and return the minimal element

  val peek (q: t) : elt
    ensures { minimal_elt result q.elts }
    raises  { Empty -> q.elts = Nil }

return the minimal element, without modifying the queue

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

empty the queue

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

return a fresh copy of the queue

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

check whether the queue is empty

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

return the number of elements in the queue

end

Simpler interface

when duplicate elements are not allowed

module PqueueNoDup

Types

  type elt

the abstract type of elements

  clone export relations.TotalOrder with type t = elt

elt is equipped with a total order rel

  use import set.Fset

  type t model { mutable elts: set elt }

the priority queue is modeled as a finite set of elements


Operations

  val create () : t ensures { result.elts = empty }

create a fresh, empty queue

  val push (x: elt) (q: t) : unit writes {q}
    ensures { q.elts = add x (old q.elts) }

push an element in a queue

  exception Empty

exception raised by pop and peek to signal an empty queue

  predicate minimal_elt (x: elt) (s: set elt) =
     mem x s /\ forall e: elt. mem e s -> rel x e

property of the element returned by pop and peek

  val pop (q: t) : elt writes {q}
    ensures { q.elts = remove result (old q.elts) }
    ensures { minimal_elt result (old q.elts) }
    raises  { Empty -> q.elts = (old q.elts) = empty }

remove and returns the minimal element

  val peek (q: t) : elt
    ensures { minimal_elt result q.elts }
    raises  { Empty -> q.elts = empty }

return the minimal element, without modifying the queue

  val clear (q: t) : unit writes {q} ensures {q.elts = empty }

empty the queue

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

return a fresh copy of the queue

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

check whether the queue is empty

  val length (q: t) : int
    ensures { result = cardinal q.elts }

return the number of elements in the queue

end

Generated by why3doc 0.88.0