stdlib/pqueue.mlw

   1 (** {1 Priority queues} *)
   2
   3 (** {2 Polymorphic mutable priority queues} *)
   4
   5 module Pqueue
   6
   7   (** {3 Types} *)
   8
   9   type elt
  10   (** the abstract type of elements *)
  11
  12   predicate le elt elt
  13   (** `elt` is equipped with a total pre order `le` *)
  14
  15   clone export relations.TotalPreOrder
  16     with type t = elt, predicate rel = le, axiom .
  17
  18   use int.Int
  19   use seq.Seq
  20   use seq.Occ
  21
  22   (** the priority queue is modeled as a sorted sequence of elements *)
  23   type t = abstract { mutable elts: seq elt }
  24     invariant { forall i1 i2.
  25                 0 <= i1 <= i2 < length elts -> le elts[i1] elts[i2] }
  26   meta coercion function elts
  27
  28   (** {3 Operations} *)
  29
  30   val create () : t ensures { result = empty }
  31   (** create a fresh, empty queue *)
  32
  33   val push (x: elt) (q: t) : unit
  34     writes  { q }
  35     ensures { length q = 1 + length (old q) }
  36     ensures { occ_all x q = 1 + occ_all x (old q) }
  37     ensures { forall y. y <> x -> occ_all y q = occ_all y (old q) }
  38   (** push an element in a queue *)
  39
  40   exception Empty
  41   (** exception raised by `pop` and `peek` to signal an empty queue *)
  42
  43   val pop (q: t) : elt
  44     writes {q}
  45     ensures { length (old q) > 0 }
  46     ensures { result = (old q)[0] }
  47     ensures { q = (old q)[1..] }
  48     raises  { Empty -> q = old q = empty }
  49   (** remove and return the minimal element *)
  50
  51   val safe_pop (q: t) : elt
  52     requires { length q > 0 }
  53     writes   { q }
  54     ensures  { result = (old q)[0] }
  55     ensures  { q = (old q)[1..] }
  56   (** remove and return the minimal element *)
  57
  58   val peek (q: t) : elt
  59     ensures { length q > 0 }
  60     ensures { result = q[0] }
  61     raises  { Empty -> q = empty }
  62   (** return the minimal element, without modifying the queue *)
  63
  64   val safe_peek (q: t) : elt
  65     requires { length q > 0 }
  66     ensures { result = q[0] }
  67   (** return the minimal element, without modifying the queue *)
  68
  69   val clear (q: t) : unit
  70     writes  { q }
  71     ensures { q = empty }
  72   (** empty the queue *)
  73
  74   val copy (q: t) : t
  75     ensures { result == q }
  76   (** return a fresh copy of the queue *)
  77
  78   val is_empty (q: t) : bool
  79     ensures { result <-> q = empty }
  80   (** check whether the queue is empty *)
  81
  82   val length (q: t) : int
  83     ensures { result = length q }
  84   (** return the number of elements in the queue *)
  85
  86 end
  87
  88 (** Test the interface above using an external heapsort *)
  89 module Harness
  90
  91   use int.Int
  92   use array.Array
  93   use array.IntArraySorted
  94   use array.ArrayPermut
  95   use map.Occ as MO
  96   use seq.Seq
  97   use seq.FreeMonoid
  98   use seq.Occ as SO
  99
 100   clone Pqueue as PQ with type elt = int, predicate le = (<=)
 101
 102   let heapsort (a: array int) : unit
 103     ensures { sorted a }
 104     ensures { permut_all (old a) a }
 105   = let n = length a in
 106     let pq = PQ.create () in
 107     for i = 0 to n - 1 do
 108       invariant { length pq = i }
 109       invariant { forall x. MO.occ x a.elts 0 n =
 110                   MO.occ x a.elts i n + SO.occ_all x pq }
 111       PQ.push (Array.([]) a i) pq
 112     done;
 113     for i = 0 to n - 1 do
 114       invariant { length pq = n - i }
 115       invariant { sorted_sub a 0 i }
 116       invariant { forall j k. 0 <= j < i -> 0 <= k < length pq ->
 117                   Array.([]) a j <= pq[k] }
 118       invariant { forall x. MO.occ x (old a.elts) 0 n =
 119                   MO.occ x a.elts 0 i + SO.occ_all x pq }
 120       a[i] <- PQ.safe_pop pq
 121     done
 122
 123 end
 124
 125 (** {2 Simpler interface}
 126
 127 when duplicate elements are not allowed
 128
 129 *)
 130
 131 module PqueueNoDup
 132
 133   (** {3 Types} *)
 134
 135   type elt
 136   (** the abstract type of elements *)
 137
 138   predicate le elt elt
 139   (** `elt` is equipped with a total pre order `le` *)
 140
 141   clone export relations.TotalPreOrder
 142     with type t = elt, predicate rel = le, axiom .
 143
 144   use set.Fset
 145
 146   type t = abstract { mutable elts: fset elt }
 147   (** the priority queue is modeled as a finite set of elements *)
 148   meta coercion function elts
 149
 150   (** {3 Operations} *)
 151
 152   val create () : t
 153     ensures { result = empty }
 154   (** create a fresh, empty queue *)
 155
 156   val push (x: elt) (q: t) : unit
 157     writes  { q }
 158     ensures { q = add x (old q) }
 159   (** push an element in a queue *)
 160
 161   exception Empty
 162   (** exception raised by `pop` and `peek` to signal an empty queue *)
 163
 164   predicate minimal_elt (x: elt) (s: fset elt) =
 165      mem x s /\ forall e: elt. mem e s -> le x e
 166   (** property of the element returned by `pop` and `peek` *)
 167
 168   val pop (q: t) : elt
 169     writes  { q }
 170     ensures { q = remove result (old q) }
 171     ensures { minimal_elt result (old q) }
 172     raises  { Empty -> q = old q = empty }
 173   (** remove and returns the minimal element *)
 174
 175   val safe_pop (q: t) : elt
 176     writes  { q }
 177     requires { not q = empty }
 178     ensures { q = remove result (old q) }
 179     ensures { minimal_elt result (old q) }
 180   (** remove and returns the minimal element *)
 181
 182   val peek (q: t) : elt
 183     ensures { minimal_elt result q }
 184     raises  { Empty -> q = empty }
 185   (** return the minimal element, without modifying the queue *)
 186
 187   val safe_peek (q: t) : elt
 188     requires { not q = empty }
 189     ensures { minimal_elt result q }
 190   (** return the minimal element, without modifying the queue *)
 191
 192   val clear (q: t) : unit
 193     writes  { q }
 194     ensures { q = empty }
 195   (** empty the queue *)
 196
 197   val copy (q: t) : t
 198     ensures { result = q }
 199   (** return a fresh copy of the queue *)
 200
 201   val is_empty (q: t) : bool
 202     ensures { result <-> q = empty }
 203   (** check whether the queue is empty *)
 204
 205   val length (q: t) : int
 206     ensures { result = cardinal q }
 207   (** return the number of elements in the queue *)
 208
 209 end