examples/counting_sort.mlw

   1
   2 (* Counting Sort.
   3
   4    We sort an array of integers, assuming all elements are in the range 0..k-1
   5
   6    We simply count the elements equal to x, for each
   7    x in 0..k-1, and then (re)fill the array with two nested loops.
   8
   9    TODO: Implement and prove a *stable* variant of counting sort,
  10    as proposed in
  11
  12       Introduction to Algorithms
  13       Cormen, Leiserson, Rivest
  14       The MIT Press (2nd edition)
  15       Section 9.2, page 175
  16 *)
  17
  18 module Spec
  19
  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   val constant k: int
  27     ensures { 0 < result }
  28
  29   predicate k_values (a: array int) =
  30     forall i: int. 0 <= i < length a -> 0 <= a[i] < k
  31
  32   (* we introduce two predicates:
  33      - [numeq a v l u] is the number of values in a[l..u[ equal to v
  34      - [numlt a v l u] is the number of values in a[l..u[ less than v *)
  35   function numeq (a: array int) (v i j : int) : int =
  36     N.numof (fun k -> a[k] = v) i j
  37
  38   function numlt (a: array int) (v i j : int) : int =
  39     N.numof (fun k -> a[k] < v) i j
  40
  41   (* an ovious lemma relates numeq and numlt *)
  42   let rec lemma eqlt (a: array int) (v: int) (l u: int)
  43     requires { k_values a }
  44     requires { 0 <= v < k }
  45     requires { 0 <= l < u <= length a }
  46     ensures  { numlt a v l u + numeq a v l u = numlt a (v+1) l u }
  47     variant  { u - l }
  48   = if l < u-1 then eqlt a v (l+1) u
  49
  50   (* permutation of two arrays is here conveniently defined using [numeq]
  51      i.e. as the equality of the two multi-sets *)
  52   predicate permut (a b: array int) =
  53     length a = length b /\
  54     forall v: int. 0 <= v < k -> numeq a v 0 (length a) = numeq b v 0 (length b)
  55
  56 end
  57
  58 module CountingSort
  59
  60   use Spec
  61   use 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     ensures  { sorted b /\ permut a b }
  67   = let c = Array.make k 0 in
  68     for i = 0 to length a - 1 do
  69       invariant { forall v: int. 0 <= v < k -> c[v] = numeq a v 0 i }
  70       let v = a[i] in
  71       c[v] <- c[v] + 1
  72     done;
  73     let j = ref 0 in
  74     for v = 0 to k-1 do
  75       invariant { !j = numlt a v 0 (length a) }
  76       invariant { sorted_sub b 0 !j }
  77       invariant { forall e: int. 0 <= e < !j -> 0 <= b[e] < v }
  78       invariant { forall f: int.
  79         0 <= f < v -> numeq b f 0 !j = numeq a f 0 (length a) }
  80       for i = 1 to c[v] do
  81         invariant { !j -i+1 = numlt a v 0 (length a) }
  82         invariant { sorted_sub b 0 !j }
  83         invariant { forall e: int. 0 <= e < !j -> 0 <= b[e] <= v }
  84         invariant { forall f: int.
  85           0 <= f < v -> numeq b f 0 !j = numeq a f 0 (length a) }
  86         invariant { numeq b v 0 !j = i-1 }
  87         b[!j] <- v;
  88         incr j
  89       done
  90     done;
  91     assert { !j = length b }
  92
  93 end
  94
  95 module InPlaceCountingSort
  96
  97   use Spec
  98   use ref.Refint
  99
 100   (* sorts array a in place *)
 101   let in_place_counting_sort (a: array int)
 102     requires { k_values a }
 103     ensures  { sorted a /\ permut (old a) a }
 104   = let c = make k 0 in
 105     for i = 0 to length a - 1 do
 106       invariant { forall v: int. 0 <= v < k -> c[v] = numeq a v 0 i }
 107       let v = a[i] in
 108       c[v] <- c[v] + 1
 109     done;
 110     let j = ref 0 in
 111     for v = 0 to k-1 do
 112       invariant { !j = numlt (old a) v 0 (length a) }
 113       invariant { sorted_sub a 0 !j }
 114       invariant { forall e: int. 0 <= e < !j -> 0 <= a[e] < v }
 115       invariant { forall f: int.
 116         0 <= f < v -> numeq a f 0 !j = numeq (old a) f 0 (length a) }
 117       for i = 1 to c[v] do
 118         invariant { !j -i+1 = numlt (old a) v 0 (length a) }
 119         invariant { sorted_sub a 0 !j }
 120         invariant { forall e: int. 0 <= e < !j -> 0 <= a[e] <= v }
 121         invariant { forall f: int.
 122           0 <= f < v -> numeq a f 0 !j = numeq (old a) f 0 (length a) }
 123         invariant { numeq a v 0 !j = i-1 }
 124         a[!j] <- v;
 125         incr j;
 126         assert {forall f. 0 <= f < v -> numeq a f 0 !j = numeq a f 0 (!j - 1)}
 127       done
 128     done;
 129     assert { !j = length a }
 130
 131 end
 132
 133 module Harness
 134
 135   use Spec
 136   use InPlaceCountingSort
 137
 138   let harness ()
 139     requires { k = 2 }
 140   = (* a is [0;1;0] *)
 141     let a = make 3 0 in
 142     a[1] <- 1;
 143     in_place_counting_sort a;
 144     (* a is now [0;0;1] *)
 145     assert { numeq a 0 0 3 = 2 };
 146     assert { numeq a 1 0 3 = 1 };
 147     assert { a[0] = 0 };
 148     assert { a[1] = 0 };
 149     assert { a[2] = 1 }
 150
 151 end