heapsort.mlw 1.23 KB
Newer Older
1 2 3 4 5 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

module HeapSort

(**** logic declarations *****)
use import int.Int
use import elements.Elements
use import bag.Bag
use import bag_of_integers.Bag_integers

use import module ref.Ref
use import module array.Array
use import module array.ArraySorted
use import module abstract_heap.AbstractHeap

lemma Min_of_sorted:
  forall a:M.map int int, i n :int.
    0 <= i < n -> (M.sorted_sub a 0 n) ->
      min_bag (elements a i n) = M.get a i

(* heap sort *)

let heapSort (a : array int) =
  { length a >= 0 }
  'Init:
  let len = length a in
  let h = create len in

   for i = 0 to len-1 do
    invariant
      { 0 <= i <= len /\
        card (model !h) = i /\
	model !h = elements a.elts 0 i }
  insert h a[i]
  done;

  for i = 0 to len-1 do
   invariant
     { 0 <= i <= len /\
       card (model !h) = len - i /\
       elements (at a.elts 'Init) 0 len =
         union (model !h) (elements a.elts 0 i) /\
       sorted_sub a 0 i /\
       forall j:int. 0 <= j < i -> a[j] <= min_bag (model !h)
     }
   a[i] <- extractMin h;
   assert { a[i] <=  min_bag (model !h) }
  done
  { sorted a /\
    elements a.elts 0 (length a) =
      elements (old a.elts) 0 (length a) }

end

(*
Local Variables:
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
56
compile-command: "why3ide -I . heapsort.mlw"
57 58 59 60 61 62 63 64 65 66 67
End:
*)