pqueue.mlw 4.47 KB
Newer Older
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
1

2
(* Polymorphic mutable priority queues. *)
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
3 4 5

module Pqueue

6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71
  type elt

  (* [elt] is equipped with a total order [rel] *)
  clone export relations.TotalOrder with type t = elt

  (* the priority queue is modeled as a list of elements *)
  use import list.List
  use import list.Mem
  use import list.Permut
  use import list.Length

  type t model {| mutable elts: list elt |}

  (* Operations. *)

  (* creates a fresh, empty queue *)
  val create: unit -> {} t { result.elts = Nil }

  (* pushes an element in a queue *)
  val push:
    x: elt -> q: t ->
    { }
    unit writes q
    { q.elts = Cons x (old q.elts) }

  (* exception raised by pop and peek to signal an empty queue *)
  exception Empty

  (* pop and peek return the minimal element, defined as follows *)
  predicate minimal_elt (x: elt) (s: list elt) =
     mem x s /\ forall e: elt. mem e s -> rel x e

  (* removes and returns the minimal element *)
  val pop:
    q: t ->
    {}
    elt
    writes q raises Empty
    { permut (Cons result q.elts) (old q.elts) /\
      minimal_elt result (old q.elts) }
    | Empty -> { q.elts = (old q.elts) = Nil }

  (* returns the minimal element, without modifying the queue *)
  val peek:
    q: t ->
    {}
    elt
    reads q raises Empty
    { minimal_elt result q.elts } | Empty -> { q.elts = Nil }

  (* empties the queue *)
  val clear: q: t -> {} unit writes q {q.elts = Nil }

  (* returns a fresh copy of the queue *)
  val copy: q: t -> {} t reads q { result = q }

  (* checks whether the queue is empty *)
  val is_empty:
    q: t -> {} bool reads q { result=True <-> q.elts = Nil }

  (* returns the number of elements in the queue *)
  val length: q: t -> {} int reads q { result = length q.elts }

end

module Test
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
72

73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104
  use import list.List
  use import module Pqueue as P

  function v1 : elt
  function v2 : elt
  axiom values: rel v2 v1 /\ v1 <> v2

  let test0 () =
    let s = P.create () : P.t in
    assert { s.elts = Nil };
    let b = P.is_empty s in
    assert { b = True };
    let n = P.length s in
    assert { n = 0 }

  let test1 () =
    let s = P.create () in
    P.push v1 s;
    let x = P.peek s in assert { x = v1 };
    P.push v2 s;
    let x = P.peek s in assert { x = v2 };
    ()

end

(* Simpler interface when duplicate elements are not allowed *)

module PqueueNoDup

  (* Types. *)

  (* the abstract type of elements *)
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
105 106
  type elt

107 108 109 110 111
  (* [elt] is equipped with a total order [rel] *)
  clone export relations.TotalOrder with type t = elt

  (* the priority queue is modeled as a finite set of elements *)
  use import set.Fset
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
112 113 114

  type t model {| mutable elts: set elt |}

115 116 117
  (* Operations. *)

  (* creates a fresh, empty queue *)
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
118 119
  val create: unit -> {} t { result.elts = empty }

120
  (* pushes an element in a queue *)
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
121 122 123 124 125 126
  val push:
    x: elt -> q: t ->
    { }
    unit writes q
    { q.elts = add x (old q.elts) }

127
  (* exception raised by pop and peek to signal an empty queue *)
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
128 129
  exception Empty

130 131 132 133 134
  (* pop and peek return the minimal element, defined as follows *)
  predicate minimal_elt (x: elt) (s: set elt) =
     mem x s /\ forall e: elt. mem e s -> rel x e

  (* removes and returns the minimal element *)
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
135 136 137 138 139
  val pop:
    q: t ->
    {}
    elt
    writes q raises Empty
140
    { q.elts = remove result (old q.elts) /\ minimal_elt result (old q.elts) }
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
141 142
    | Empty -> { q.elts = (old q.elts) = empty }

143
  (* returns the minimal element, without modifying the queue *)
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
144 145 146 147 148
  val peek:
    q: t ->
    {}
    elt
    reads q raises Empty
149
    { minimal_elt result q.elts } | Empty -> { q.elts = empty }
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
150

151
  (* empties the queue *)
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
152 153
  val clear: q: t -> {} unit writes q {q.elts = empty }

154
  (* returns a fresh copy of the queue *)
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
155 156
  val copy: q: t -> {} t reads q { result = q }

157
  (* checks whether the queue is empty *)
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
158 159 160
  val is_empty:
    q: t -> {} bool reads q { result=True <-> q.elts = empty }

161
  (* returns the number of elements in the queue *)
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
162 163 164 165
  val length: q: t -> {} int reads q { result = cardinal q.elts }

end

166
module TestNoDup
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
167 168

  use import set.Fset
169
  use import module PqueueNoDup as P
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
170 171 172

  function v1 : elt
  function v2 : elt
173
  axiom values: rel v2 v1 /\ v1 <> v2
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
174 175

  let test0 () =
176
    let s = P.create () : P.t in
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
177
    assert { s.elts = empty };
178
    let b = P.is_empty s in
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
179
    assert { b = True };
180
    let n = P.length s in
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
181 182 183
    assert { n = 0 }

  let test1 () =
184 185 186 187 188
    let s = P.create () in
    P.push v1 s;
    let x = P.peek s in assert { x = v1 };
    P.push v2 s;
    let x = P.peek s in assert { x = v2 };
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
189 190 191 192 193 194 195 196 197
    ()

end

(*
Local Variables:
compile-command: "unset LANG; make -C .. modules/pqueue"
End:
*)