## VerifyThis 2017: Odd-even transposition sort (alt)

solution to VerifyThis 2017 challenge 3

Auteurs: Raphaël Rieu-Helft / Mário Pereira

Catégories: Array Data Structure / Sorting Algorithms

Outils: Why3

Références: VerifyThis @ ETAPS 2017

see also the index (by topic, by tool, by reference, by year)

```use map.Map
use array.Array
use array.IntArraySorted
use array.ArrayPermut
use array.ArraySwap
use int.Int
use ref.Refint
use int.Sum
use number.Parity

let ghost function array_max (a:array int) : int
ensures  { forall j. 0 <= j < length a -> a[j] <= result }
= if length a = 0 then 0
else
let m = ref a[0] in
let i = ref 0 in
while !i < length a do
variant   { length a - !i }
invariant { 0 <= !i <= length a }
invariant { forall j. 0 <= j < !i -> a[j] <= !m }
if a[!i] > !m then m := a[!i];
incr i
done;
!m

function aux (a:int -> int) (m i:int) : int = i * (m - Map.get a i)

lemma aux_pos :
forall a m i. 0 <= i < length a -> a[i] <= m -> aux a.elts m i >= 0

function entropy (a:array int) (m:int) : int = sum (aux a.elts m) 0 (length a)

let rec lemma entropy_pos (a:array int) (m i:int)
requires { 0 <= i <= length a }
requires { forall j. 0 <= j < i <= length a -> a[j] <= m }
ensures { sum (aux a.elts m) 0 i >= 0 }
variant { i }
=
if i > 0
then begin
entropy_pos a m (i-1);
assert { aux a.elts m (i-1) >= 0 };
assert { sum (aux a.elts m) 0 i
= sum (aux a.elts m) 0 (i-1) + aux a.elts m (i-1) };
end
else ()

let lemma decompose_entropy (a:int -> int) (i j m n:int)
requires { 0 <= i < j < n }
ensures  { sum (aux a m) 0 n
= sum (aux a m) 0 i + sum (aux a m) (j+1) n
+ sum (aux a m) (i+1) j + aux a m i + aux a m j }
=  let decomp (i j k: int)
requires { 0 <= i <= j <= k <= n }
ensures  { sum (aux a m) i k = sum (aux a m) i j + sum (aux a m) j k }
= () in
decomp 0 i n; decomp i (j+1) n; decomp i j (j+1); decomp i (i+1) j

let lemma inst_ext (a1 a2: int -> int) (a b m:int)
requires { forall i. a <= i < b -> Map.get a1 i = Map.get a2 i }
ensures { sum (aux a1 m) a b = sum (aux a2 m) a b }
= assert { forall i. a <= i < b -> (aux a1 m) i = (aux a2 m) i }

let my_swap (a:array int) (i j:int) (ghost m:int)
requires { a[i] > a[j] }
requires { 0 <= i < j < length a }
writes   { a }
ensures  { exchange (old a) a i j }
ensures  { entropy a m < entropy (old a) m }
= let ghost a1 = a.elts in
decompose_entropy a1 i j m a.length;
swap a i j;
let ghost a2 = a.elts in
assert { a[i] * i + a[j] * j > a[i] * j + a[j] * i
by a[j] - a[i] > 0 /\ j - i > 0
so a[i] * i + a[j] * j - (a[i] * j + a[j] * i)
= (a[j] - a[i]) * (j-i)
> 0 };
decompose_entropy a2 i j m a.length;
assert { aux a2 m i + aux a2 m j < aux a1 m i + aux a1 m j
by (old a)[i] = a[j]
so (old a)[j] = a[i]
so aux a2 m i + aux a2 m j
= (m - a[i]) * i + (m - a[j]) * j
= m * (i+j) - (a[i] * i + a[j] * j)
< m * (i+j) - (a[i] * j + a[j] * i)
= (m - a[j]) * i + (m - a[i]) * j
= aux a1 m i + aux a1 m j
};
inst_ext a1 a2 0 i m; inst_ext a1 a2 (i+1) j m; inst_ext a1 a2 (j+1) a.length m

let rec lemma local_order_implies_sort_sub (a:array int) (i j:int)
requires { forall k. i <= k < j - 1 -> a[k] <= a[k+1] }
requires { 0 <= i <= j <= length a }
ensures  { sorted_sub a i j }
variant  { j - i }
= if i < j - 1
then begin
local_order_implies_sort_sub a (i+1) j;
assert { forall k l. i <= k <= l < j -> a[k] <= a[l]
by k = l \/  i = k < l \/  i+1 <= k < j };
end

let odd_even_sort (a: array int)
requires { length a > 0 }
ensures  { sorted a }
ensures  { permut_all (old a) a }
=
let ghost m = array_max a in
let ok = ref false in
while not !ok do
variant   { entropy a m + (if !ok then 0 else 1) }
invariant { permut_all (old a) a }
invariant { !ok -> sorted a }
ok := true;
label L in
let i = ref 1 in
while !i < length a - 1 do
variant   { length a - !i }
invariant { permut_all (old a) a }
invariant { 0 <= !i <= length a }
invariant { odd !i }
invariant { !ok -> entropy a m = entropy (a at L) m }
invariant { !ok -> forall j. 0 <= j < !i -> odd j
-> a[j] <= a[j+1] }
invariant { not !ok -> entropy a m < entropy (a at L) m }
if a[!i] > a[!i+1]
then begin my_swap a !i (!i+1) m; ok := false end;
i := !i + 2
done;
let i = ref 0 in
while !i < length a - 1 do
variant   { length a - !i }
invariant { permut_all (old a) a }
invariant { 0 <= !i <= length a }
invariant { even !i }
invariant { !ok -> entropy a m = entropy (a at L) m }
invariant { !ok -> forall j. 0 <= j < length a - 1 /\ odd j
-> a[j] <= a[j+1] }
invariant { !ok -> forall j. 0 <= j < !i /\ even j
-> a[j] <= a[j+1] }
invariant { not !ok -> entropy a m < entropy (a at L) m }
if a[!i] > a[!i+1]
then begin my_swap a !i (!i+1) m; ok := false end;
i := !i + 2
done;
done;```

# Why3 Proof Results for Project "verifythis_2017_odd_even_sort_rearranging"

## Theory "verifythis_2017_odd_even_sort_rearranging.Top": fully verified

 Obligations Alt-Ergo 2.0.0 CVC3 2.4.1 Z3 4.7.1 VC for array_max --- --- --- split_goal_right postcondition 0.01 --- --- index in array bounds 0.01 --- --- loop invariant init 0.01 --- --- loop invariant init 0.01 --- --- index in array bounds 0.01 --- --- index in array bounds 0.00 --- --- loop variant decrease 0.01 --- --- loop invariant preservation 0.01 --- --- loop invariant preservation 0.01 --- --- loop variant decrease 0.01 --- --- loop invariant preservation 0.01 --- --- loop invariant preservation 0.01 --- --- postcondition 0.00 --- --- aux_pos --- --- 0.02 VC for entropy_pos --- --- --- split_goal_right variant decrease 0.01 --- --- precondition 0.00 --- --- precondition 0.01 --- --- assertion 0.02 --- --- assertion 0.01 --- --- postcondition 0.01 --- --- VC for decompose_entropy --- --- --- split_goal_right postcondition 0.02 --- --- precondition 0.01 --- --- precondition 0.01 --- --- precondition 0.01 --- --- precondition 0.01 --- --- postcondition 0.14 --- --- VC for inst_ext --- --- --- split_goal_right assertion 0.01 --- --- postcondition 0.19 --- --- VC for my_swap --- --- --- split_goal_right precondition 0.02 --- --- precondition 0.01 --- --- assertion --- --- --- split_goal_right VC for my_swap 0.03 --- --- VC for my_swap 0.02 --- --- VC for my_swap 0.01 --- --- VC for my_swap --- 0.08 --- VC for my_swap 0.02 --- --- precondition 0.01 --- --- assertion --- --- --- split_goal_right VC for my_swap 0.04 --- --- VC for my_swap 0.03 --- --- VC for my_swap 0.02 --- --- VC for my_swap 0.04 --- --- VC for my_swap 0.01 --- --- VC for my_swap 0.01 --- --- VC for my_swap 0.02 --- --- VC for my_swap 0.02 --- --- precondition 0.79 --- --- precondition 0.68 --- --- precondition 4.20 --- --- postcondition 0.01 --- --- postcondition 0.02 --- --- VC for local_order_implies_sort_sub --- --- --- split_goal_right variant decrease 0.01 --- --- precondition 0.01 --- --- precondition 0.01 --- --- assertion 0.02 --- --- postcondition 0.01 --- --- VC for odd_even_sort --- --- --- split_goal_right loop invariant init 0.01 --- --- loop invariant init 0.01 --- --- loop invariant init 0.01 --- --- loop invariant init 0.01 --- --- loop invariant init 0.01 --- --- loop invariant init 0.00 --- --- loop invariant init 0.01 --- --- loop invariant init 0.01 --- --- index in array bounds 0.02 --- --- index in array bounds 0.01 --- --- precondition 0.01 --- --- precondition 0.01 --- --- loop variant decrease 0.01 --- --- loop invariant preservation 0.26 --- --- loop invariant preservation 0.01 --- --- loop invariant preservation 0.02 --- --- loop invariant preservation 0.01 --- --- loop invariant preservation 0.10 --- --- loop invariant preservation 0.02 --- --- loop variant decrease 0.01 --- --- loop invariant preservation 0.01 --- --- loop invariant preservation 0.01 --- --- loop invariant preservation 0.01 --- --- loop invariant preservation 0.01 --- --- loop invariant preservation 0.02 --- --- loop invariant preservation 0.02 --- --- loop invariant init 0.01 --- --- loop invariant init 0.01 --- --- loop invariant init 0.01 --- --- loop invariant init 0.02 --- --- loop invariant init 0.10 --- --- loop invariant init 0.01 --- --- loop invariant init 0.01 --- --- index in array bounds 0.01 --- --- index in array bounds 0.02 --- --- precondition 0.01 --- --- precondition 0.01 --- --- loop variant decrease 0.01 --- --- loop invariant preservation 0.37 --- --- loop invariant preservation 0.01 --- --- loop invariant preservation 0.02 --- --- loop invariant preservation 0.01 --- --- loop invariant preservation 0.02 --- --- loop invariant preservation 0.02 --- --- loop invariant preservation 0.01 --- --- loop variant decrease 0.01 --- --- loop invariant preservation 0.02 --- --- loop invariant preservation 0.01 --- --- loop invariant preservation 0.02 --- --- loop invariant preservation 0.02 --- --- loop invariant preservation 0.02 --- --- loop invariant preservation 0.01 --- --- loop invariant preservation 0.01 --- --- loop variant decrease --- --- 0.10 loop invariant preservation 0.01 --- --- loop invariant preservation 0.18 --- --- postcondition 0.00 --- --- postcondition 0.01 --- ---