counting_sort.mlw 4.34 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19

(* Counting Sort.

   We sort an array of integers, assuming all elements are in the range 0..k-1

   We simply count the elements equal to x, for each
   x in 0..k-1, and then (re)fill the array with two nested loops.

   TODO: Implement and prove a *stable* variant of counting sort,
   as proposed in

      Introduction to Algorithms
      Cormen, Leiserson, Rivest
      The MIT Press (2nd edition)
      Section 9.2, page 175
*)

module Spec

20
  use export int.Int
21
  use int.NumOf as N
22
  use export array.Array
23
  use export array.IntArraySorted
24 25

  (* values of the array are in the range 0..k-1 *)
26
  constant k: int
27 28 29 30 31 32 33 34
  axiom k_positive: 0 < k

  predicate k_values (a: array int) =
    forall i: int. 0 <= i < length a -> 0 <= a[i] < k

  (* we introduce two predicates:
     - [numeq a v l u] is the number of values in a[l..u[ equal to v
     - [numlt a v l u] is the number of values in a[l..u[ less than v *)
35 36
  function numeq (a: array int) (v i j : int) : int =
    N.numof (\ k. a[k] = v) i j
37

38 39
  function numlt (a: array int) (v i j : int) : int =
    N.numof (\ k. a[k] < v) i j
40 41

  (* an ovious lemma relates numeq and numlt *)
42 43 44 45 46 47 48
  let rec lemma eqlt (a: array int) (v: int) (l u: int)
    requires { k_values a }
    requires { 0 <= v < k }
    requires { 0 <= l < u <= length a }
    ensures  { numlt a v l u + numeq a v l u = numlt a (v+1) l u }
    variant  { u - l }
  = if l < u-1 then eqlt a v (l+1) u
49 50 51 52 53 54 55 56 57 58 59

  (* permutation of two arrays is here conveniently defined using [numeq]
     i.e. as the equality of the two multi-sets *)
  predicate permut (a b: array int) =
    length a = length b /\
    forall v: int. 0 <= v < k -> numeq a v 0 (length a) = numeq b v 0 (length b)

end

module CountingSort

60 61
  use import Spec
  use import ref.Refint
62 63

  (* sorts array a into array b *)
64
  let counting_sort (a: array int) (b: array int)
65
    requires { k_values a /\ length a = length b }
66 67
    ensures  { sorted b /\ permut a b }
  = let c = make k 0 in
68 69 70 71 72 73 74
    for i = 0 to length a - 1 do
      invariant { forall v: int. 0 <= v < k -> c[v] = numeq a v 0 i }
      let v = a[i] in
      c[v] <- c[v] + 1
    done;
    let j = ref 0 in
    for v = 0 to k-1 do
75 76 77 78 79
      invariant { !j = numlt a v 0 (length a) }
      invariant { sorted_sub b 0 !j }
      invariant { forall e: int. 0 <= e < !j -> 0 <= b[e] < v }
      invariant { forall f: int.
        0 <= f < v -> numeq b f 0 !j = numeq a f 0 (length a) }
80
      for i = 1 to c[v] do
81 82 83 84 85 86
        invariant { !j -i+1 = numlt a v 0 (length a) }
        invariant { sorted_sub b 0 !j }
        invariant { forall e: int. 0 <= e < !j -> 0 <= b[e] <= v }
        invariant { forall f: int.
          0 <= f < v -> numeq b f 0 !j = numeq a f 0 (length a) }
        invariant { numeq b v 0 !j = i-1 }
87 88 89 90 91 92 93 94 95 96
        b[!j] <- v;
        incr j
      done
    done;
    assert { !j = length b }

end

module InPlaceCountingSort

97 98
  use import Spec
  use import ref.Refint
99 100

  (* sorts array a in place *)
101
  let in_place_counting_sort (a: array int)
102
    requires { k_values a }
103 104
    ensures  { sorted a /\ permut (old a) a }
  = 'L:
105 106 107 108 109 110 111 112
    let c = make k 0 in
    for i = 0 to length a - 1 do
      invariant { forall v: int. 0 <= v < k -> c[v] = numeq a v 0 i }
      let v = a[i] in
      c[v] <- c[v] + 1
    done;
    let j = ref 0 in
    for v = 0 to k-1 do
113 114 115 116 117
      invariant { !j = numlt (at a 'L) v 0 (length a) }
      invariant { sorted_sub a 0 !j }
      invariant { forall e: int. 0 <= e < !j -> 0 <= a[e] < v }
      invariant { forall f: int.
        0 <= f < v -> numeq a f 0 !j = numeq (at a 'L) f 0 (length a) }
118
      for i = 1 to c[v] do
119 120 121 122 123 124
        invariant { !j -i+1 = numlt (at a 'L) v 0 (length a) }
        invariant { sorted_sub a 0 !j }
        invariant { forall e: int. 0 <= e < !j -> 0 <= a[e] <= v }
        invariant { forall f: int.
          0 <= f < v -> numeq a f 0 !j = numeq (at a 'L) f 0 (length a) }
        invariant { numeq a v 0 !j = i-1 }
125
        a[!j] <- v;
Clément Fumex's avatar
Clément Fumex committed
126 127
        incr j;
        assert {forall f. 0 <= f < v -> numeq a f 0 !j = numeq a f 0 (!j - 1)}
128 129 130 131 132 133 134 135
      done
    done;
    assert { !j = length a }

end

module Harness

136 137
  use import Spec
  use import InPlaceCountingSort
138

MARCHE Claude's avatar
MARCHE Claude committed
139 140 141
  let harness ()
    requires { k = 2 }
  = (* a is [0;1;0] *)
142 143 144
    let a = make 3 0 in
    a[1] <- 1;
    in_place_counting_sort a;
MARCHE Claude's avatar
MARCHE Claude committed
145
    (* a is now [0;0;1] *)
146 147 148 149 150 151 152
    assert { numeq a 0 0 3 = 2 };
    assert { numeq a 1 0 3 = 1 };
    assert { a[0] = 0 };
    assert { a[1] = 0 };
    assert { a[2] = 1 }

end