Priority queues

Polymorphic mutable priority queues

module Pqueue

Types

  type elt

the abstract type of elements

  predicate le elt elt

elt is equipped with a total pre order le

  clone export relations.TotalPreOrder
    with type t = elt, predicate rel = le, axiom .

  use int.Int
  use seq.Seq
  use seq.Occ

  type t = abstract { mutable elts: seq elt }
    invariant { forall i1 i2.
                0 <= i1 <= i2 < length elts -> le elts[i1] elts[i2] }
  meta coercion function elts

the priority queue is modeled as a sorted sequence of elements

Operations

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

create a fresh, empty queue

  val push (x: elt) (q: t) : unit
    writes  { q }
    ensures { length q = 1 + length (old q) }
    ensures { occ_all x q = 1 + occ_all x (old q) }
    ensures { forall y. y <> x -> occ_all y q = occ_all y (old q) }

push an element in a queue

  exception Empty

exception raised by pop and peek to signal an empty queue

  val pop (q: t) : elt
    writes {q}
    ensures { length (old q) > 0 }
    ensures { result = (old q)[0] }
    ensures { q = (old q)[1..] }
    raises  { Empty -> q = old q = empty }

remove and return the minimal element

  val safe_pop (q: t) : elt
    requires { length q > 0 }
    writes   { q }
    ensures  { result = (old q)[0] }
    ensures  { q = (old q)[1..] }

remove and return the minimal element

  val peek (q: t) : elt
    ensures { length q > 0 }
    ensures { result = q[0] }
    raises  { Empty -> q = empty }

return the minimal element, without modifying the queue

  val safe_peek (q: t) : elt
    requires { length q > 0 }
    ensures { result = q[0] }

return the minimal element, without modifying the queue

  val clear (q: t) : unit
    writes  { q }
    ensures { q = 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 <-> q = empty }

check whether the queue is empty

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

return the number of elements in the queue

end

module Harness

Test the interface above using an external heapsort

  use int.Int
  use array.Array
  use array.IntArraySorted
  use array.ArrayPermut
  use map.Occ as MO
  use seq.Seq
  use seq.FreeMonoid
  use seq.Occ as SO

  clone Pqueue as PQ with type elt = int, predicate le = (<=)

  let heapsort (a: array int) : unit
    ensures { sorted a }
    ensures { permut_all (old a) a }
  = let n = length a in
    let pq = PQ.create () in
    for i = 0 to n - 1 do
      invariant { length pq = i }
      invariant { forall x. MO.occ x a.elts 0 n =
                  MO.occ x a.elts i n + SO.occ_all x pq }
      PQ.push (Array.([]) a i) pq
    done;
    for i = 0 to n - 1 do
      invariant { length pq = n - i }
      invariant { sorted_sub a 0 i }
      invariant { forall j k. 0 <= j < i -> 0 <= k < length pq ->
                  Array.([]) a j <= pq[k] }
      invariant { forall x. MO.occ x (old a.elts) 0 n =
                  MO.occ x a.elts 0 i + SO.occ_all x pq }
      a[i] <- PQ.safe_pop pq
    done

end

Simpler interface

when duplicate elements are not allowed

module PqueueNoDup

Types

  type elt

the abstract type of elements

  predicate le elt elt

elt is equipped with a total pre order le

  clone export relations.TotalPreOrder
    with type t = elt, predicate rel = le, axiom .

  use set.Fset

  type t = abstract { mutable elts: fset elt }

the priority queue is modeled as a finite set of elements

  meta coercion function elts

Operations

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

create a fresh, empty queue

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

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: fset elt) =
     mem x s /\ forall e: elt. mem e s -> le x e

property of the element returned by pop and peek

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

remove and returns the minimal element

  val safe_pop (q: t) : elt
    writes  { q }
    requires { not q = empty }
    ensures { q = remove result (old q) }
    ensures { minimal_elt result (old q) }

remove and returns the minimal element

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

return the minimal element, without modifying the queue

  val safe_peek (q: t) : elt
    requires { not q = empty }
    ensures { minimal_elt result q }

return the minimal element, without modifying the queue

  val clear (q: t) : unit
    writes  { q }
    ensures { q = 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 <-> q = empty }

check whether the queue is empty

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

return the number of elements in the queue

end