examples_in_progress/simple_priority_queue.mlw

   1
   2 (* Simple priority queue implementation
   3    (inspired by Tinelli's lecture http://www.divms.uiowa.edu/~tinelli/181/) *)
   4
   5 module SimplePrioriyQueue
   6
   7   use int.Int
   8   use ref.Ref
   9   use array.Array
  10   use bag.Bag
  11
  12   type elt
  13   val function priority elt : int
  14
  15   use array.NumOfEq
  16
  17   type t = {
  18     elems: array elt;
  19     mutable size : int; (* size elements, stored in elems[0..size[ *)
  20     mutable h    : int; (* index of the highest priority element, if any *)
  21     ghost mutable bag: bag elt;
  22   }
  23   invariant { 0 <= size <= elems.length }
  24   invariant { size = 0 \/ 0 <= h < size }
  25   invariant { forall e: elt.
  26               numof elems e 0 size = nb_occ e bag }
  27   invariant { size > 0 -> forall e: elt. mem e bag ->
  28               priority e <= priority elems[h] }
  29
  30   lemma numof_occ:
  31     forall a: array elt, e: elt, l u: int.
  32     numof a e l u > 0 <-> exists i: int. l <= i < u /\ a[i] = e
  33
  34   lemma numof_add:
  35     forall a: array elt, e: elt, l u: int. l <= u ->
  36     e = a[u] -> numof a e l (u+1) = 1 + numof a e l u
  37
  38   let create (n: int) (dummy: elt) : t
  39     requires { 0 <= n }
  40     ensures  {result. size = 0 }
  41   = { elems = Array.make n dummy; size = 0; h = 0; bag = empty_bag }
  42
  43   predicate is_empty (q: t) = q.size = 0
  44
  45   predicate is_full (q: t) = q.size = length q.elems
  46
  47   let add (q: t) (x: elt) : unit
  48     requires { not (is_full q) }
  49     writes   { q.elems.elts, q.h, q.size, q.bag }
  50     ensures  { q.bag = add x (old q.bag) }
  51   = q.elems[q.size] <- x;
  52     if q.size = 0 then
  53       q.h <- 0
  54     else if priority x > priority q.elems[q.h] then
  55       q.h <- q.size;
  56     q.size <- q.size + 1;
  57     q.bag <- add x q.bag
  58
  59   let highest (q: t) : elt
  60     requires { not (is_empty q) }
  61     ensures  { mem result q.bag }
  62     ensures  { forall e: elt. mem e q.bag -> priority e <= priority result }
  63   = q.elems[q.h]
  64
  65   let remove (q: t) : elt
  66     requires { not (is_empty q) }
  67     writes   { q.elems.elts, q.h, q.size, q.bag }
  68     ensures  { old q.bag = add result q.bag }
  69     ensures  { mem result q.bag }
  70     ensures  { forall e: elt. mem e q.bag -> priority e <= priority result }
  71   = q.size <- q.size - 1;
  72     let r = q.elems[q.h] in
  73     q.elems[q.h] <- q.elems[q.size];
  74     if q.size > 0 then begin
  75       let m = ref (priority q.elems[0]) in
  76       q.h <- 0;
  77       for i = 1 to q.size - 1 do
  78         invariant { 0 <= q.h < q.size }
  79         invariant { forall j: int. 0 <= j < i ->
  80                     priority q.elems[j] <= priority q.elems[q.h] }
  81         let p = priority q.elems[i] in
  82         if p > !m then begin q.h <- i; m := p end
  83       done
  84     end;
  85     q.bag <- diff q.bag (singleton r);
  86     r
  87
  88 end
  89