Wiki Agenda Contact Version française

VerifyThis 2017: Odd-even transposition sort (alt)

solution to VerifyThis 2017 challenge 3


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

Topics: Array Data Structure / Sorting Algorithms

Tools: Why3

References: 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;

download ZIP archive

Why3 Proof Results for Project "verifythis_2017_odd_even_sort_rearranging"

Theory "verifythis_2017_odd_even_sort_rearranging.Top": fully verified

ObligationsAlt-Ergo 1.30CVC3 2.4.1Z3 4.5.0
VC array_max---------
split_goal_right
VC array_max.00.01------
VC array_max.10.01------
VC array_max.20.01------
VC array_max.30.01------
VC array_max.40.01------
VC array_max.50.00------
VC array_max.60.01------
VC array_max.70.01------
VC array_max.80.01------
VC array_max.90.01------
VC array_max.100.01------
VC array_max.110.01------
VC array_max.120.00------
aux_pos------0.56
VC entropy_pos---------
split_goal_right
VC entropy_pos.00.01------
VC entropy_pos.10.00------
VC entropy_pos.20.01------
VC entropy_pos.30.02------
VC entropy_pos.40.01------
VC entropy_pos.50.01------
VC decompose_entropy---------
split_goal_right
VC decompose_entropy.00.02------
VC decompose_entropy.10.01------
VC decompose_entropy.20.01------
VC decompose_entropy.30.01------
VC decompose_entropy.40.01------
VC decompose_entropy.50.14------
VC inst_ext---------
split_goal_right
VC inst_ext.00.01------
VC inst_ext.10.19------
VC my_swap---------
split_goal_right
VC my_swap.00.01------
VC my_swap.10.01------
VC my_swap.2---------
split_goal_right
VC my_swap.2.00.03------
VC my_swap.2.10.02------
VC my_swap.2.20.01------
VC my_swap.2.3---0.08---
VC my_swap.2.40.02------
VC my_swap.30.02------
VC my_swap.4---------
split_goal_right
VC my_swap.4.00.04------
VC my_swap.4.10.03------
VC my_swap.4.20.02------
VC my_swap.4.30.02------
VC my_swap.4.40.01------
VC my_swap.4.50.01------
VC my_swap.4.60.04------
VC my_swap.4.70.02------
VC my_swap.50.50------
VC my_swap.60.52------
VC my_swap.74.10------
VC my_swap.80.01------
VC my_swap.90.02------
VC local_order_implies_sort_sub---------
split_goal_right
VC local_order_implies_sort_sub.00.01------
VC local_order_implies_sort_sub.10.01------
VC local_order_implies_sort_sub.20.01------
VC local_order_implies_sort_sub.30.02------
VC local_order_implies_sort_sub.40.01------
VC odd_even_sort---------
split_goal_right
VC odd_even_sort.00.01------
VC odd_even_sort.10.01------
VC odd_even_sort.20.01------
VC odd_even_sort.30.01------
VC odd_even_sort.40.01------
VC odd_even_sort.50.00------
VC odd_even_sort.60.01------
VC odd_even_sort.70.01------
VC odd_even_sort.80.01------
VC odd_even_sort.90.01------
VC odd_even_sort.100.01------
VC odd_even_sort.110.01------
VC odd_even_sort.120.01------
VC odd_even_sort.130.09------
VC odd_even_sort.140.01------
VC odd_even_sort.150.01------
VC odd_even_sort.160.02------
VC odd_even_sort.170.01------
VC odd_even_sort.180.01------
VC odd_even_sort.190.01------
VC odd_even_sort.200.01------
VC odd_even_sort.210.01------
VC odd_even_sort.220.02------
VC odd_even_sort.230.01------
VC odd_even_sort.240.02------
VC odd_even_sort.250.01------
VC odd_even_sort.260.01------
VC odd_even_sort.270.01------
VC odd_even_sort.280.01------
VC odd_even_sort.290.02------
VC odd_even_sort.300.01------
VC odd_even_sort.310.10------
VC odd_even_sort.320.01------
VC odd_even_sort.330.02------
VC odd_even_sort.340.02------
VC odd_even_sort.350.01------
VC odd_even_sort.360.01------
VC odd_even_sort.370.01------
VC odd_even_sort.380.26------
VC odd_even_sort.390.01------
VC odd_even_sort.400.02------
VC odd_even_sort.410.01------
VC odd_even_sort.420.10------
VC odd_even_sort.430.02------
VC odd_even_sort.440.02------
VC odd_even_sort.450.01------
VC odd_even_sort.460.02------
VC odd_even_sort.470.01------
VC odd_even_sort.480.02------
VC odd_even_sort.490.01------
VC odd_even_sort.500.02------
VC odd_even_sort.510.02------
VC odd_even_sort.520.02------
VC odd_even_sort.53------0.10
VC odd_even_sort.540.01------
VC odd_even_sort.551.73------
VC odd_even_sort.560.00------
VC odd_even_sort.570.01------