# Quicksort with Bentley-Bull trick

in 0.82, Coq used 2 times to prove:

• sorted a (i+1) n needs lemma with sorted_div_sorted. (Coq uses lemma proved by Alt-ergo
• permut (postcondition) needs permut_weakening
• Z3 used (after inline transformation) in 2nd partition assertion.

in 0.83, fully automatic but with combining Alt-ergo, Yices, Z3.

```module QuickSort

use import int.Int
use import ref.Ref
use import array.Array
use import array.IntArraySorted
use import array.ArrayPermut
use import array.ArrayEq

predicate div_sub (a: array int) (l m u: int) =
(forall i: int. l <= i < m -> a[i] <= a[m]) /\
(forall j: int. m+1 <= j < u -> a[m] <= a[j])

lemma sorted_div_sorted_sub:
forall a: array int. forall l m u : int.
sorted_sub a l m -> div_sub a l m u -> sorted_sub a (m+1) u
-> sorted_sub a l u

lemma permut_sub_trans:
forall a1 a2 a3: array 'a, l u: int.
permut_sub a1 a2 l u -> permut_sub a2 a3 l u ->
permut_sub a1 a3 l u

let swap (a: array int) (i: int) (j: int) =
requires { 0 <= i < length a /\ 0 <= j < length a }
ensures { exchange (old a) a i j }
let v = a[i] in
a[i] <- a[j];
a[j] <- v

let rec quick_sort1 (a: array int) lo hi =
requires { 0 <= lo <= length a /\ 0 <= hi <= length a }
ensures { sorted_sub a lo hi /\ permut_sub (old a) a lo hi}
'L:
if lo < hi - 1 then begin
let i = ref (lo + 1) in
for j = lo + 1 to hi - 1 do
invariant { lo < !i <= j }
invariant {forall k: int. lo+1 <= k < !i ->  a[k] <= a[lo]}
invariant {forall k': int. !i <= k' < j -> a[lo] <= a[k']}
invariant {permut_sub (at a 'L) a (lo+1) hi}
if a[j] < a[lo] then begin
swap a !i j;
i := !i + 1
end
done;
assert {permut_sub (at a 'L) a lo hi };
swap a lo (!i-1);
assert {permut_sub (at a 'L) a lo hi };
assert {div_sub a lo (!i-1) hi };
quick_sort1 a lo (!i - 1);
assert {permut_sub (at a 'L) a lo hi };
assert {div_sub a lo (!i-1) hi };
quick_sort1 a !i hi;
assert {permut_sub (at a 'L) a lo hi };
assert {div_sub a lo (!i-1) hi }
end

let quick_sort (a: array int) =
ensures { sorted a /\ permut_all (old a) a}
quick_sort1 a 0 (Array.length a)

end
```

• Generated by why3doc 0.85