Wiki Agenda Contact English version

VerifyThis 2017: Odd-even transposition sort

solution to VerifyThis 2017 challenge 3


Auteurs: Jean-Christophe Filliâtre

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)


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 2.0.0Z3 4.11.2
VC for odd_even_sorted------
split_goal_right
loop invariant init0.01---
assertion------
split_goal_right
assertion0.02---
VC for odd_even_sorted0.02---
VC for odd_even_sorted0.01---
loop invariant preservation0.01---
postcondition0.01---
VC for odd_even_transposition_sort------
split_goal_right
loop invariant init0.00---
loop invariant init0.01---
loop invariant init0.01---
loop invariant init0.01---
loop invariant init0.01---
loop invariant init0.01---
index in array bounds0.01---
index in array bounds0.01---
precondition0.01---
loop variant decrease0.01---
loop invariant preservation0.01---
loop invariant preservation0.34---
loop invariant preservation0.22---
loop invariant preservation0.04---
loop variant decrease0.01---
loop invariant preservation0.01---
loop invariant preservation0.01---
loop invariant preservation0.01---
loop invariant preservation0.01---
assertion0.01---
loop invariant init0.01---
loop invariant init0.01---
loop invariant init0.01---
loop invariant init0.01---
loop invariant init0.01---
loop invariant init0.02---
loop invariant init0.01---
index in array bounds0.01---
index in array bounds0.01---
precondition0.02---
loop variant decrease0.01---
loop invariant preservation0.01---
loop invariant preservation0.01---
loop invariant preservation0.22---
loop invariant preservation0.01---
loop invariant preservation0.77---
loop invariant preservation0.12---
loop invariant preservation0.02---
loop variant decrease0.01---
loop invariant preservation0.01---
loop invariant preservation0.01---
loop invariant preservation0.07---
loop invariant preservation0.01---
loop invariant preservation0.02---
loop invariant preservation0.01---
loop invariant preservation0.08---
assertion0.02---
loop variant decrease---0.05
loop invariant preservation0.01---
loop invariant preservation0.03---
postcondition0.01---
postcondition0.01---