The ProVal team was stopped at the end of August 2012, and reborn into a new team Toccata
These pages do not evolve anymore, please follow the link above for up-to-date informations about our team.

## 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.

Authors: Jean-Christophe Filliâtre

Topics: Array Data Structure

Tools: Why3

```
(* 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

use import int.Int
use export array.Array
use export array.ArraySorted

(* values of the array are in the range 0..k-1 *)
function k: int
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 *)
type param = (array int, int)

predicate eq (p: param) (i: int) = let (a,v) = p in a[i] = v
clone int.NumOfParam as Neq with type param = param, predicate pr = eq
function numeq (a: array int) (v i j : int) : int = Neq.num_of (a, v) i j

predicate lt (p: param) (i: int) = let (a,v) = p in a[i] < v
clone int.NumOfParam as Nlt with type param = param, predicate pr = lt
function numlt (a: array int) (v i j : int) : int = Nlt.num_of (a, v) i j

(* an ovious lemma relates numeq and numlt *)
lemma eqlt:
forall a: array int. k_values a ->
forall v: int. 0 <= v < k ->
forall l u: int. 0 <= l < u <= length a ->
numlt a v l u + numeq a v l u = numlt a (v+1) l u

(* 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

use import Spec
use import ref.Refint

(* sorts array a into array b *)
let counting_sort (a: array int) (b: array int)
requires { k_values a /\ 0 <= length a = length b }
ensures  { sorted b /\ permut a b }
= 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
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) }
for i = 1 to c[v] do
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 }
b[!j] <- v;
incr j
done
done;
assert { !j = length b }

end

module InPlaceCountingSort

use import Spec
use import ref.Refint

(* sorts array a in place *)
let in_place_counting_sort (a: array int)
requires { k_values a /\ 0 <= length a }
ensures  { sorted a /\ permut (old a) a }
= 'L:
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
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) }
for i = 1 to c[v] do
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 }
a[!j] <- v;
incr j
done
done;
assert { !j = length a }

end

module Harness

use import Spec
use import InPlaceCountingSort

let harness () requires { k = 2 } =
(* a is [0;1;0] *)
let a = make 3 0 in
a[1] <- 1;
in_place_counting_sort a;
(* b is now [0;0;1] *)
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
```