Wiki Agenda Contact Version française

VerifyThis 2017: Odd-even transposition sort

solution to VerifyThis 2017 challenge 3


Authors: Jean-Christophe Filliâtre

Topics: Array Data Structure / Sorting Algorithms

Tools: Why3

References: VerifyThis @ ETAPS 2017

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


VerifyThis @ ETAPS 2017 competition Challenge 3: Odd-Even Transposition Sort

See https://formal.iti.kit.edu/ulbrich/verifythis2017/

Author: Jean-Christophe FilliĆ¢tre (CNRS)

(* note: this is only a solution for the sequential (single processor) version
   of the challenge *)

module Challenge3

  use int.Int
  use int.ComputerDivision
  use ref.Refint
  use array.Array
  use array.IntArraySorted
  use array.ArraySwap
  use array.ArrayPermut
  use array.Inversions

  (* odd-sorted up to n exclusive *)
  predicate odd_sorted (a: array int) (n: int) =
    forall i. 0 <= i -> 2*i + 2 < n -> a[2*i+1] <= a[2*i+2]

  (* even-sorted up to n exclusive *)
  predicate even_sorted (a: array int) (n: int) =
    forall i. 0 <= i -> 2*i + 1 < n -> a[2*i] <= a[2*i+1]

  let lemma odd_even_sorted (a: array int) (n: int)
    requires { 0 <= n <= length a }
    requires { odd_sorted a n }
    requires { even_sorted a n }
    ensures  { sorted_sub a 0 n }
  = if n > 0 && length a > 0 then
    for i = 1 to n - 1 do
      invariant { sorted_sub a 0 i }
      assert { forall j. 0 <= j < i -> a[j] <= a[i]
                  by a[i-1] <= a[i]
                  by i-1 = 2 * div (i-1) 2 \/
                     i-1 = 2 * div (i-1) 2 + 1 }
    done

  (* note: program variable "sorted" renamed into "is_sorted"
     (clash with library predicate "sorted" on arrays) *)
  let odd_even_transposition_sort (a: array int)
    ensures { sorted a }
    ensures { permut_all (old a) a }
  = let is_sorted = ref false in
    while not !is_sorted do
      invariant { permut_all (old a) a }
      invariant { !is_sorted -> sorted a }
      variant   { (if !is_sorted then 0 else 1), inversions a }
      is_sorted := true;
      let i = ref 1 in
      let ghost half_i = ref 0 in
      label L in
      while !i < length a - 1 do
        invariant { 0 <= !half_i /\ 0 <= !i = 2 * !half_i + 1 }
        invariant { permut_all (old a) a }
        invariant { odd_sorted a !i }
        invariant { if !is_sorted then inversions a = inversions (a at L)
                                  else inversions a < inversions (a at L) }
        variant   { length a - !i }
        if a[!i] > a[!i+1] then begin
          swap a !i (!i+1);
          is_sorted := false;
        end;
        i := !i + 2;
        ghost half_i := !half_i + 1
      done;
      assert { odd_sorted a (length a) };
      i := 0;
      ghost half_i := 0;
      while !i < length a - 1 do
        invariant { 0 <= !half_i /\ 0 <= !i = 2 * !half_i }
        invariant { 0 <= !i }
        invariant { permut_all (old a) a }
        invariant { !is_sorted -> odd_sorted a (length a) }
        invariant { even_sorted a !i }
        invariant { if !is_sorted then inversions a = inversions (a at L)
                                  else inversions a < inversions (a at L) }
        invariant { !is_sorted \/ inversions a < inversions (a at L) }
        variant   { length a - !i }
        if a[!i] > a[!i+1] then begin
          swap a !i (!i+1);
          is_sorted := false;
        end;
        i := !i + 2;
        ghost half_i := !half_i + 1
      done;
      assert { !is_sorted -> even_sorted a (length a) }
    done

end

download ZIP archive

Why3 Proof Results for Project "verifythis_2017_odd_even_transposition_sort"

Theory "verifythis_2017_odd_even_transposition_sort.Challenge3": fully verified

ObligationsAlt-Ergo 1.30Z3 4.4.0
VC odd_even_sorted------
split_goal_right
VC odd_even_sorted.00.01---
VC odd_even_sorted.1------
split_goal_right
VC odd_even_sorted.1.00.02---
VC odd_even_sorted.1.10.02---
VC odd_even_sorted.1.20.01---
VC odd_even_sorted.20.01---
VC odd_even_sorted.30.01---
VC odd_even_transposition_sort------
split_goal_right
VC odd_even_transposition_sort.00.00---
VC odd_even_transposition_sort.10.01---
VC odd_even_transposition_sort.20.01---
VC odd_even_transposition_sort.30.01---
VC odd_even_transposition_sort.40.01---
VC odd_even_transposition_sort.50.01---
VC odd_even_transposition_sort.60.01---
VC odd_even_transposition_sort.70.01---
VC odd_even_transposition_sort.80.02---
VC odd_even_transposition_sort.90.01---
VC odd_even_transposition_sort.100.01---
VC odd_even_transposition_sort.110.12---
VC odd_even_transposition_sort.120.08---
VC odd_even_transposition_sort.130.01---
VC odd_even_transposition_sort.140.01---
VC odd_even_transposition_sort.150.01---
VC odd_even_transposition_sort.160.01---
VC odd_even_transposition_sort.170.01---
VC odd_even_transposition_sort.180.01---
VC odd_even_transposition_sort.190.01---
VC odd_even_transposition_sort.200.01---
VC odd_even_transposition_sort.210.01---
VC odd_even_transposition_sort.220.01---
VC odd_even_transposition_sort.230.01---
VC odd_even_transposition_sort.240.01---
VC odd_even_transposition_sort.250.02---
VC odd_even_transposition_sort.260.01---
VC odd_even_transposition_sort.270.01---
VC odd_even_transposition_sort.280.01---
VC odd_even_transposition_sort.290.01---
VC odd_even_transposition_sort.300.01---
VC odd_even_transposition_sort.310.01---
VC odd_even_transposition_sort.320.01---
VC odd_even_transposition_sort.330.25---
VC odd_even_transposition_sort.340.01---
VC odd_even_transposition_sort.350.21---
VC odd_even_transposition_sort.360.04---
VC odd_even_transposition_sort.370.08---
VC odd_even_transposition_sort.380.01---
VC odd_even_transposition_sort.390.01---
VC odd_even_transposition_sort.400.01---
VC odd_even_transposition_sort.410.07---
VC odd_even_transposition_sort.420.01---
VC odd_even_transposition_sort.430.02---
VC odd_even_transposition_sort.440.01---
VC odd_even_transposition_sort.450.02---
VC odd_even_transposition_sort.460.02---
VC odd_even_transposition_sort.47---0.12
VC odd_even_transposition_sort.480.07---
VC odd_even_transposition_sort.490.03---
VC odd_even_transposition_sort.500.01---
VC odd_even_transposition_sort.510.01---