priority_queue.mlw 13 KB
Newer Older
1 2 3 4 5 6

(** {1 Logarithmic-time mergeable priority queues implementation on top
       of AVL trees}
    Author: Martin Clochard *)

module PQueue
7

8 9 10 11 12 13 14 15
  use import int.Int
  use import avl.SelectionTypes
  use import option.Option
  use import ref.Ref
  use import list.List
  use import list.Append
  use import list.Mem
  use import list.Length
16

17
  (** {2 Implementation parameters} *)
18

19 20 21
  (** Balancing level is kept abstract. *)
  constant balancing : int
  axiom balancing_positive : balancing > 0
22

23 24 25 26 27 28 29
  (** The Elements of the priority queue are indexed by totally ordered keys.
      Moreover, this order can be effectively decided. *)
  namespace D type t 'a end
  namespace K type t end
  clone export key_type.ProgramKeyType with type t = D.t, type key = K.t
  constant default_element : D.t 'a
  clone preorder.Computable as CO with type t = K.t
30

31
  (** {2 Instantiation of the AVL tree module} *)
32

33 34 35 36 37
  clone sorted.Increasing as S with type K.t = D.t,
    type K.key = K.t,
    function K.key = key,
    predicate O.rel = CO.le,
    goal O.Trans
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 72 73 74 75 76 77 78 79 80 81 82
  (** Use the minimum monoid to measure sequence of elements by their
      minimum value. We extend it with a minimum element in order to measure
      empty sequences. *)
  namespace M
    type t = option K.t
    constant zero : t = None
    function op (x y:t) : t = match x with
      | None -> y
      | Some a -> match y with
        | None -> x
        | Some b -> if CO.lt a b
          then x
          else y
        end
      end
    let lemma assoc_m (x y z:t) : unit
      ensures { op x (op y z) = op (op x y) z }
    = match x , y , z with
      | None , _ , _ -> assert { true }
      | _ , None , _ -> assert { true }
      | _ , _ , None -> assert { true }
      | _ -> ()
      end
    let lemma neutral_m (x:t) : unit
      ensures { op x zero = x = op zero x }
    = match x with None -> () | _ -> assert { true } end
    clone export monoid.Monoid with type t = t,
      constant zero = zero,function op = op,lemma assoc,lemma neutral
    clone export monoid.MonoidSumDef with type M.t = t,
      constant M.zero = zero,function M.op = op,goal M.assoc,goal M.neutral
    let zero () : t
      ensures { result = None }
    = None
    let op (x y:t) : t
      ensures { result = op x y }
    = match x with
      | None -> y
      | Some a -> match y with
        | None -> x
        | Some b -> if CO.compare a b < 0
          then x
          else y
        end
      end
83

84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102
  end
  (** Elements are measured by their keys. *)
  namespace D
    (* Morally equivalent to
       [function measure (d:D.t 'a) : M.t = Some d.key],
       but left axiomatized for technical reasons. *)
    (*** Using a definition here triggers a minor glitch which makes
         some goals logically unprovable (sound but incomplete behaviour).
         It is caused by a harmful interference between inlining during WP
         and the current treatment of higher-order objects.
         Note: if some purist want to eliminate such axioms, that is still
         possible by performing one more step of cloning over the current
         module. *)
    function measure (d:D.t 'a) : M.t
    axiom measure_def : forall d:D.t 'a. measure d = Some d.key
    let measure (d:D.t 'a) : M.t
      ensures { result = measure d }
    = Some (get_key d)
  end
103

104 105 106
  (** In priority queue, we are looking for the minimum element.
      No extra information is required to perform such search. *)
  type selector = unit
107

108
  (** We can only select the minimum in a non-empty sequeuence. *)
109

110
  predicate selection_possible 'e (l:list 'g) = l <> Nil
111

112 113
  predicate lower_bound_strict (x:K.t) (l:list (D.t 'a)) =
    (forall y. mem y l -> CO.lt x y.key)
114

115 116 117 118 119 120 121 122 123 124
  (** We are interested in split where the middle element
      is the minimum of the sequence. In order to make sure
      that the same element is returned at each search, we enforce
      that such split corresponds exactly to the first occurrence. *)
  predicate selected 'e (e:split (D.t 'a)) =
      match e.middle with
      | None -> false
      | Some d -> S.lower_bound d.key e.right /\
        lower_bound_strict d.key e.left
      end
125

126 127 128 129 130 131 132 133 134
  (** The summary of a sequence is indeed its minimum element. *)
  let rec lemma monoid_sum_is_min (l:list (D.t 'a)) : unit
    ensures { let x = M.sum D.measure l in
      match x with
      | None -> l = Nil
      | Some a -> S.lower_bound a l /\ (exists d. mem d l /\ CO.eq d.key a)
      end }
    variant { l }
  = match l with Cons _ q -> monoid_sum_is_min q | _ -> () end
135

136 137 138 139 140 141 142 143 144 145
  (** The middle element of a selected split is indeed the minimum. *)
  let lemma selected_is_min (s:'d) (e:split (D.t 'a)) : unit
    requires { selected s e }
    ensures { let l = rebuild e in match e.middle with
      | None -> false
      | Some d -> S.lower_bound d.key l && match M.sum D.measure l with
        | None -> false
        | Some k -> CO.eq d.key k
        end
      end }
146 147 148 149
  = match e.middle with
    | None -> absurd
    | Some d -> assert { S.lower_bound d.key e.right && CO.le d.key d.key }
    end
150

151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178
  let selected_part (ghost llis:list (D.t 'a))
    (ghost rlis:list (D.t 'a))
    (s:unit) (sl:M.t) (d:D.t 'a) (sr:M.t) : part_base unit
    requires { sl = M.sum D.measure llis /\ sr = M.sum D.measure rlis }
    returns { Here -> let e2 = { left = llis;
        middle = Some d;
        right = rlis } in selected s e2
      | Left sl -> selection_possible sl llis /\
        forall e. selected sl e /\ rebuild e = llis ->
          selected s (right_extend e d rlis)
      | Right sr -> selection_possible sr rlis /\
        forall e. selected sr e /\ rebuild e = rlis ->
          selected s (left_extend llis d e) }
  = let kd = get_key d in
    monoid_sum_is_min llis;
    monoid_sum_is_min rlis;
    match sl , sr with
    | None , None -> Here
    | None , Some a -> if CO.compare kd a <= 0 then Here else Right ()
    | Some a , None -> if CO.compare kd a < 0 then Here else Left ()
    | Some a , Some b -> if CO.compare kd b <= 0
      then if CO.compare a kd <= 0
        then Left ()
        else Here
      else if CO.compare a b <= 0
      then Left ()
      else Right ()
    end
179

180 181 182 183 184 185 186 187
  (** Extract the first minimum element of a sequence. *)
  function first_minimum_acc (acc:D.t 'a) (l:list (D.t 'a)) : D.t 'a =
    match l with
    | Nil -> acc
    | Cons x q -> if CO.le acc.key x.key
      then first_minimum_acc acc q
      else first_minimum_acc x q
    end
188

189 190 191 192
  function first_minimum (l:list (D.t 'a)) : D.t 'a = match l with
    | Nil -> default_element
    | Cons x q -> first_minimum_acc x q
    end
193

194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222
  (** the first_minimum function and the selected predicate both
      describe the minimum element. *)
  let rec lemma first_minimum_caracterisation (e:split (D.t 'a)) : unit
    requires { e.middle <> None /\ selected () e }
    ensures { match e.middle with
      | Some x -> first_minimum (rebuild e) = x
      | None -> false
      end }
    variant { e.right }
  = let mid = match e.middle with None -> absurd | Some x -> x end in
    let rec aux (e:split (D.t 'a)) : unit
      requires { e.middle = Some mid /\ selected () e }
      ensures { forall acc:D.t 'a.
        CO.lt mid.key acc.key -> first_minimum_acc acc (rebuild e) = mid }
      variant { length e.left + length e.right }
    = match e.left with
      | Nil -> match e.right with
        | Nil -> ()
        | Cons _ q -> aux { e with right = q }
        end
      | Cons _ q -> aux { e with left = q }
      end in
    match e.left with
    | Nil -> match e.right with
      | Nil -> ()
      | Cons _ q -> first_minimum_caracterisation { e with right = q }
      end
    | Cons _ q -> aux { e with left = q }
    end
223

224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244
  (** Full instantiation of the avl module. *)
  clone avl.AVL as Sel with type selector = selector,
    predicate selection_possible = selection_possible,
    predicate selected = selected,
    val selected_part = selected_part,
    goal selection_empty,
    constant balancing = balancing,
    goal balancing_positive,
    type D.t = D.t,
    function D.measure = D.measure,
    val D.measure = D.measure,
    type M.t = M.t,
    constant M.zero = M.zero,
    function M.op = M.op,
    goal M.assoc,
    goal M.neutral,
    function M.sum = M.sum,
    goal M.sum_def_nil,
    goal M.sum_def_cons,
    val M.zero = M.zero,
    val M.op = M.op
245

246
  (** {2 Adaptation of specification to priority queues} *)
247

248
  type t 'a = Sel.t 'a
249

250 251 252
  (** Model: a bag of data with a minimum element.
     The point of the minimum is that we want the returned minimum element
     to be always the same, modulo preorder equivalence is not enough. *)
253

254 255 256 257 258
  type m 'a = {
    bag : D.t 'a -> int;
    minimum : D.t 'a;
    card : int;
  }
259

260
  (** Convert a list to a bag. *)
261
  constant empty_bag : 'a -> int = \_:'a. 0
262 263
  function add_bag (x:'a) (f:'a -> int) : 'a -> int =
    \y:'a. if y = x then f y + 1 else f y
264

265 266 267 268
  function as_bag (l:list 'a) : 'a -> int = match l with
    | Nil -> empty_bag
    | Cons x q -> add_bag x (as_bag q)
    end
269

270 271 272 273 274
  (** A few lemmas about the bag representation of a list. *)
  let rec lemma as_bag_append (l r:list 'a) : unit
    ensures { forall x:'a. as_bag (l++r) x = as_bag l x + as_bag r x }
    variant { l }
  = match l with Nil -> () | Cons _ q -> as_bag_append q r end
275

276 277 278 279
  let rec lemma as_bag_bounds (l:list 'a) : unit
    ensures { forall x:'a. 0 <= as_bag l x <= length l }
    variant { l }
  = match l with Nil -> () | Cons _ q -> as_bag_bounds q end
280

281 282 283 284
  let rec lemma as_bag_membership (d:'a) (l:list 'a) : unit
    ensures { as_bag l d > 0 <-> mem d l }
    variant { l }
  = match l with Nil -> () | Cons _ q -> as_bag_membership d q end
285

286 287 288 289 290
  (** Convert the avl tree to logical model. *)
  function m (t:t 'a) : m 'a =
    { bag = as_bag t.Sel.m.Sel.lis;
      card = length t.Sel.m.Sel.lis;
      minimum = first_minimum t.Sel.m.Sel.lis }
291

292 293 294 295 296
  let ghost m (t:t 'a) : m 'a
    ensures { result = t.m }
  = { bag = as_bag t.Sel.m.Sel.lis;
      card = length t.Sel.m.Sel.lis;
      minimum = first_minimum t.Sel.m.Sel.lis }
297

298 299
  (** Invariant *)
  predicate c (t:t 'a) = Sel.c t
300

301 302 303 304 305 306 307 308 309
  (** Invariant over the logical model. *)
  let lemma correction (t:t 'a) : unit
    requires { c t }
    ensures { forall d:D.t 'a. 0 <= t.m.bag d <= t.m.card }
    ensures { t.m.card >= 0 /\ (t.m.card > 0 -> t.m.bag t.m.minimum > 0) }
    ensures { forall d:D.t 'a. 0 < t.m.bag d -> CO.le t.m.minimum.key d.key }
  = if t.m.card > 0
    then let r0 = Sel.default_split () in
      let _ = Sel.split r0 () t in ()
310

311 312 313 314 315
  (** Create an empty priority queue. *)
  let empty () : t 'a
    ensures { forall d:D.t 'a. result.m.bag d = 0 }
    ensures { result.m.card = 0 /\ c result }
  = Sel.empty ()
316

317 318 319 320 321 322
  (** Create a one-element priority queue. *)
  let singleton (d:D.t 'a) : t 'a
    ensures { result.m.bag d = 1 /\
      forall d2:D.t 'a. d2 <> d -> result.m.bag d2 = 0 }
    ensures { result.m.card = 1 /\ c result }
  = Sel.singleton d
323

324 325 326 327 328 329 330 331 332 333 334 335 336
  (** Test emptyness of a priority queue. *)
  let is_empty (ghost rd:ref (D.t 'a)) (t:t 'a) : bool
    requires { c t }
    ensures { result -> forall d:D.t 'a. t.m.bag d = 0 }
    ensures { not result -> t.m.bag !rd > 0 }
    ensures { result <-> t.m.card = 0 }
  = let res = Sel.is_empty t in
    ghost if not res
    then match t.Sel.m.Sel.lis with
      | Nil -> absurd
      | Cons d _ -> rd := d
      end;
    res
337

338 339 340 341 342 343
  (** Merge two priority queues. *)
  let merge (l r:t 'a) : t 'a
    requires { c l /\ c r }
    ensures { forall d. result.m.bag d = l.m.bag d + r.m.bag d }
    ensures { result.m.card = l.m.card + r.m.card /\ c result }
  = Sel.concat l r
344

345 346 347 348 349 350
  (** Additional lemma about bag created from a list
      (removal in the middle). *)
  let lemma remove_count (l:list 'a) (d:'a) (r:list 'a) : unit
    ensures { as_bag (l ++ Cons d r) d = as_bag (l++r) d + 1 }
    ensures { forall e. e <> d -> as_bag (l++Cons d r) e = as_bag (l++r) e }
  = ()
351

352 353 354 355 356 357 358 359 360 361 362 363 364 365
  (** Get and remove minimum element. *)
  let extract_min (t:t 'a) : option (D.t 'a,t 'a)
    requires { c t }
    returns { None -> t.m.card = 0 /\ (forall d. t.m.bag d = 0)
      | Some (d,e) -> t.m.card = e.m.card + 1 /\ t.m.bag d = e.m.bag d + 1 /\
        (forall d2. d2 <> d -> t.m.bag d2 = e.m.bag d2) /\
        d = t.m.minimum /\ c e }
  = if Sel.is_empty t
    then None
    else let (o,e) = Sel.extract (Sel.default_split ()) () t in
      match o with
      | None -> absurd
      | Some d -> Some (d,e)
      end
366

367 368 369 370 371 372 373 374
  (** Get minimum element. *)
  let min (t:t 'a) : D.t 'a
    requires { t.m.card >= 1 /\ c t }
    ensures { t.m.bag result > 0 /\ t.m.card > 0 /\ result = t.m.minimum }
  = match Sel.get (Sel.default_split ()) () t with
    | None -> absurd
    | Some d -> d
    end
375

376 377 378 379 380 381 382 383 384 385
  (** Pop minimum element. *)
  let pop_min (t:t 'a) : t 'a
    requires { t.m.card >= 1 /\ c t }
    ensures { t.m.card = result.m.card + 1 /\ c result /\
      t.m.bag t.m.minimum = result.m.bag t.m.minimum + 1 /\
      (forall d2. d2 <> t.m.minimum -> t.m.bag d2 = result.m.bag d2) }
  = let r0 = Sel.default_split () in
    let res = Sel.remove r0 () t in
    assert { match !r0.middle with None -> false | Some _ -> true end };
    res
386

387 388 389 390 391 392
  let add (d:D.t 'a) (t:t 'a) : t 'a
    requires { c t }
    ensures { result.m.bag d = t.m.bag d + 1 /\
      (forall d2. d2 <> d -> result.m.bag d2 = t.m.bag d2) }
    ensures { result.m.card = t.m.card + 1 /\ c result }
  = Sel.cons d t
393

394 395
end