skew_heaps.mlw 5.08 KB
Newer Older
1

2 3 4 5 6
(** Skew heaps

    Author: Jean-Christophe Filliâtre (CNRS)
*)

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
module Heap

  use import int.Int

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

  type t

  function size t : int

  function occ elt t : int

  predicate mem (x: elt) (t: t) = occ x t > 0

  function minimum t : elt

  predicate is_minimum (x: elt) (t: t) =
    mem x t && forall e. mem e t -> le x e

  axiom min_is_min:
    forall t: t. 0 < size t -> is_minimum (minimum t) t

  val empty () : t
    ensures { size result = 0 }
    ensures { forall e. not (mem e result) }

  val size (t: t) : int
    ensures { result = size t }

  val is_empty (t: t) : bool
    ensures { result <-> size t = 0 }

  val get_min (t: t) : elt
    requires { 0 < size t }
    ensures  { result = minimum t }

  val merge (t1 t2: t) : t
    ensures  { forall e. occ e result = occ e t1 + occ e t2 }
    ensures  { size result = size t1 + size t2 }

  val add (x: elt) (t: t) : t
    ensures  { occ x result = occ x t + 1 }
    ensures  { forall e. e <> x -> occ e result = occ e t }
    ensures  { size result = size t + 1 }

  val remove_min (t: t) : t
    requires { 0 < size t }
    ensures  { occ (minimum t) result = occ (minimum t) t - 1 }
    ensures  { forall e. e <> minimum t -> occ e result = occ e t }
    ensures  { size result = size t - 1 }

end

62 63
module SkewHeaps

64
  use import int.Int
65
  use import bintree.Tree
66 67
  use export bintree.Size
  use export bintree.Occ
68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85

  type elt

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

  (* [e] is no greater than the root of [t], if any *)
  predicate le_root (e: elt) (t: tree elt) = match t with
    | Empty      -> true
    | Node _ x _ -> le e x
  end

  (* [t] is a heap *)
  predicate heap (t: tree elt) = match t with
    | Empty      -> true
    | Node l x r -> le_root x l && heap l && le_root x r && heap r
  end

86 87 88
  function minimum (tree elt) : elt
  axiom minimum_def: forall l x r. minimum (Node l x r) = x

89 90 91 92
  predicate is_minimum (x: elt) (t: tree elt) =
    mem x t && forall e. mem e t -> le x e

  (* the root is the smallest element *)
93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117
  let rec lemma root_is_min (t: tree elt) : unit
     requires { heap t && 0 < size t }
     ensures  { is_minimum (minimum t) t }
     variant  { size t }
  = match t with
    | Empty -> absurd
    | Node l _ r ->
        if l <> Empty then root_is_min l;
        if r <> Empty then root_is_min r
    end

  let empty () : tree elt
    ensures { heap result }
    ensures { size result = 0 }
    ensures { forall e. not (mem e result) }
  =
    Empty

  let is_empty (t: tree elt) : bool
    ensures { result <-> size t = 0 }
  =
    t = Empty

  let size (t: tree elt) : int
    ensures { result = size t }
118
  =
119
    size t
120 121

  let get_min (t: tree elt) : elt
122 123
    requires { heap t && 0 < size t }
    ensures  { result = minimum t }
124 125 126 127 128 129 130 131 132 133
  =
    match t with
      | Empty      -> absurd
      | Node _ x _ -> x
    end

  let rec merge (t1 t2: tree elt) : tree elt
    requires { heap t1 && heap t2 }
    ensures  { heap result }
    ensures  { forall e. occ e result = occ e t1 + occ e t2 }
134
    ensures  { size result = size t1 + size t2 }
135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150
    variant  { size t1 + size t2 }
  =
    match t1, t2 with
    | Empty, _ -> t2
    | _, Empty -> t1
    | Node l1 x1 r1, Node l2 x2 r2 ->
       if le x1 x2 then
         Node (merge r1 t2) x1 l1
       else
         Node (merge r2 t1) x2 l2
    end

  let add (x: elt) (t: tree elt) : tree elt
    requires { heap t }
    ensures  { heap result }
    ensures  { occ x result = occ x t + 1 }
151 152
    ensures  { forall e. e <> x -> occ e result = occ e t }
    ensures  { size result = size t + 1 }
153 154 155
  =
    merge (Node Empty x Empty) t

156 157
  let remove_min (t: tree elt) : tree elt
    requires { heap t && 0 < size t }
158
    ensures  { heap result }
159 160 161
    ensures  { occ (minimum t) result = occ (minimum t) t - 1 }
    ensures  { forall e. e <> minimum t -> occ e result = occ e t }
    ensures  { size result = size t - 1 }
162 163 164 165 166 167 168
  =
    match t with
      | Empty      -> absurd
      | Node l _ r -> merge l r
    end

end
169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207

(* application *)

module HeapSort

  use import SkewHeaps
  use import int.Int
  use import ref.Ref
  use import array.Array
  use import array.ArrayPermut
  clone export array.Sorted with type elt = elt, predicate le = le
  use import map.Occ as M
  use import bintree.Occ as H

  let heapsort (a: array elt) : unit
    ensures { sorted a }
    ensures { permut_all (old a) a }
  =
    let n = length a in
    let t = ref (empty ()) in
    for i = 0 to n - 1 do
      invariant { heap !t && size !t = i }
      invariant { forall e.
                  M.occ e a.elts i n + H.occ e !t = M.occ e a.elts 0 n }
      t := add a[i] !t;
      assert { M.occ a[i] a.elts i n = 1 + M.occ a[i] a.elts (i+1) n }
    done;
    'I:
    for i = 0 to n - 1 do
      invariant { sorted_sub a 0 i }
      invariant { heap !t && size !t = n - i }
      invariant { forall j. 0 <= j < i -> forall e. mem e !t -> le a[j] e }
      invariant { forall e.
                  M.occ e a.elts 0 i + H.occ e !t = M.occ e (at a.elts 'I) 0 n }
      a[i] <- get_min !t;
      t := remove_min !t
    done

end