examples/skew_heaps.mlw

   1
   2 (** Skew heaps
   3
   4     Author: Jean-Christophe Filliâtre (CNRS)
   5 *)
   6
   7 module Heap
   8
   9   use int.Int
  10
  11   type elt
  12   predicate le elt elt
  13   clone relations.TotalPreOrder with
  14     type t = elt, predicate rel = le, axiom .
  15
  16   type t
  17
  18   function size t : int
  19
  20   function occ elt t : int
  21
  22   predicate mem (x: elt) (t: t) = occ x t > 0
  23
  24   function minimum t : elt
  25
  26   predicate is_minimum (x: elt) (t: t) =
  27     mem x t && forall e. mem e t -> le x e
  28
  29   axiom min_is_min:
  30     forall t: t. 0 < size t -> is_minimum (minimum t) t
  31
  32   val constant empty : t
  33     ensures { size result = 0 }
  34     ensures { forall e. not (mem e result) }
  35
  36   val size (t: t) : int
  37     ensures { result = size t }
  38
  39   val is_empty (t: t) : bool
  40     ensures { result <-> size t = 0 }
  41
  42   val get_min (t: t) : elt
  43     requires { 0 < size t }
  44     ensures  { result = minimum t }
  45
  46   val merge (t1 t2: t) : t
  47     ensures  { forall e. occ e result = occ e t1 + occ e t2 }
  48     ensures  { size result = size t1 + size t2 }
  49
  50   val add (x: elt) (t: t) : t
  51     ensures  { occ x result = occ x t + 1 }
  52     ensures  { forall e. e <> x -> occ e result = occ e t }
  53     ensures  { size result = size t + 1 }
  54
  55   val remove_min (t: t) : t
  56     requires { 0 < size t }
  57     ensures  { occ (minimum t) result = occ (minimum t) t - 1 }
  58     ensures  { forall e. e <> minimum t -> occ e result = occ e t }
  59     ensures  { size result = size t - 1 }
  60
  61 end
  62
  63 module SkewHeaps
  64
  65   use int.Int
  66   use bintree.Tree
  67   use export bintree.Size
  68   use export bintree.Occ
  69
  70   type elt
  71
  72   val predicate le elt elt
  73   clone relations.TotalPreOrder with
  74     type t = elt, predicate rel = le, axiom .
  75
  76   (* [e] is no greater than the root of [t], if any *)
  77   predicate le_root (e: elt) (t: tree elt) = match t with
  78     | Empty      -> true
  79     | Node _ x _ -> le e x
  80   end
  81
  82   (* [t] is a heap *)
  83   predicate heap (t: tree elt) = match t with
  84     | Empty      -> true
  85     | Node l x r -> le_root x l && heap l && le_root x r && heap r
  86   end
  87
  88   function minimum (tree elt) : elt
  89   axiom minimum_def: forall l x r. minimum (Node l x r) = x
  90
  91   predicate is_minimum (x: elt) (t: tree elt) =
  92     mem x t && forall e. mem e t -> le x e
  93
  94   (* the root is the smallest element *)
  95   let rec lemma root_is_min (t: tree elt) : unit
  96      requires { heap t && 0 < size t }
  97      ensures  { is_minimum (minimum t) t }
  98      variant  { t }
  99   = match t with
 100     | Empty -> absurd
 101     | Node l _ r ->
 102         if not (is_empty l) then root_is_min l;
 103         if not (is_empty r) then root_is_min r
 104     end
 105
 106   let constant empty : tree elt = Empty
 107     ensures { heap result }
 108     ensures { size result = 0 }
 109     ensures { forall e. not (mem e result) }
 110
 111   let get_min (t: tree elt) : elt
 112     requires { heap t && 0 < size t }
 113     ensures  { result = minimum t }
 114   =
 115     match t with
 116       | Empty      -> absurd
 117       | Node _ x _ -> x
 118     end
 119
 120   let rec merge (t1 t2: tree elt) : tree elt
 121     requires { heap t1 && heap t2 }
 122     ensures  { heap result }
 123     ensures  { forall e. occ e result = occ e t1 + occ e t2 }
 124     ensures  { size result = size t1 + size t2 }
 125     variant  { size t1 + size t2 }
 126   =
 127     match t1, t2 with
 128     | Empty, _ -> t2
 129     | _, Empty -> t1
 130     | Node l1 x1 r1, Node l2 x2 r2 ->
 131        if le x1 x2 then
 132          Node (merge r1 t2) x1 l1
 133        else
 134          Node (merge r2 t1) x2 l2
 135     end
 136
 137   let add (x: elt) (t: tree elt) : tree elt
 138     requires { heap t }
 139     ensures  { heap result }
 140     ensures  { occ x result = occ x t + 1 }
 141     ensures  { forall e. e <> x -> occ e result = occ e t }
 142     ensures  { size result = size t + 1 }
 143   =
 144     merge (Node Empty x Empty) t
 145
 146   let remove_min (t: tree elt) : tree elt
 147     requires { heap t && 0 < size t }
 148     ensures  { heap result }
 149     ensures  { occ (minimum t) result = occ (minimum t) t - 1 }
 150     ensures  { forall e. e <> minimum t -> occ e result = occ e t }
 151     ensures  { size result = size t - 1 }
 152   =
 153     match t with
 154       | Empty      -> absurd
 155       | Node l _ r -> merge l r
 156     end
 157
 158 end
 159
 160 (* application *)
 161
 162 module HeapSort
 163
 164   use array.Array
 165   use array.ArrayPermut
 166   use SkewHeaps
 167   clone export array.Sorted with type elt = elt, predicate le = le, axiom .
 168   use int.Int
 169   use ref.Ref
 170   use map.Occ as M
 171   use bintree.Occ as H
 172
 173   let heapsort (a: array elt) : unit
 174     ensures { sorted a }
 175     ensures { permut_all (old a) a }
 176   =
 177     let n = length a in
 178     let t = ref empty in
 179     for i = 0 to n - 1 do
 180       invariant { heap !t && size !t = i }
 181       invariant { forall e.
 182                   M.occ e a.elts i n + H.occ e !t = M.occ e a.elts 0 n }
 183       t := add a[i] !t;
 184       assert { M.occ a[i] a.elts i n = 1 + M.occ a[i] a.elts (i+1) n }
 185     done;
 186     label I in
 187     for i = 0 to n - 1 do
 188       invariant { sorted_sub a 0 i }
 189       invariant { heap !t && size !t = n - i }
 190       invariant { forall j. 0 <= j < i -> forall e. mem e !t -> le a[j] e }
 191       invariant { forall e.
 192                   M.occ e a.elts 0 i + H.occ e !t = M.occ e (a.elts at I) 0 n }
 193       a[i] <- get_min !t;
 194       t := remove_min !t
 195     done
 196
 197 end