examples/verifythis_2017_odd_even_transposition_sort.mlw

   1 (**
   2
   3 {1 VerifyThis @ ETAPS 2017 competition
   4    Challenge 3: Odd-Even Transposition Sort}
   5
   6 See https://formal.iti.kit.edu/ulbrich/verifythis2017/
   7
   8 Author: Jean-Christophe Filliâtre (CNRS)
   9 *)
  10
  11 (* note: this is only a solution for the sequential (single processor) version
  12    of the challenge *)
  13
  14 module Challenge3
  15
  16   use int.Int
  17   use int.ComputerDivision
  18   use ref.Refint
  19   use array.Array
  20   use array.IntArraySorted
  21   use array.ArraySwap
  22   use array.ArrayPermut
  23   use array.Inversions
  24
  25   (* odd-sorted up to n exclusive *)
  26   predicate odd_sorted (a: array int) (n: int) =
  27     forall i. 0 <= i -> 2*i + 2 < n -> a[2*i+1] <= a[2*i+2]
  28
  29   (* even-sorted up to n exclusive *)
  30   predicate even_sorted (a: array int) (n: int) =
  31     forall i. 0 <= i -> 2*i + 1 < n -> a[2*i] <= a[2*i+1]
  32
  33   let lemma odd_even_sorted (a: array int) (n: int)
  34     requires { 0 <= n <= length a }
  35     requires { odd_sorted a n }
  36     requires { even_sorted a n }
  37     ensures  { sorted_sub a 0 n }
  38   = if n > 0 && length a > 0 then
  39     for i = 1 to n - 1 do
  40       invariant { sorted_sub a 0 i }
  41       assert { forall j. 0 <= j < i -> a[j] <= a[i]
  42                   by a[i-1] <= a[i]
  43                   by i-1 = 2 * div (i-1) 2 \/
  44                      i-1 = 2 * div (i-1) 2 + 1 }
  45     done
  46
  47   (* note: program variable "sorted" renamed into "is_sorted"
  48      (clash with library predicate "sorted" on arrays) *)
  49   let odd_even_transposition_sort (a: array int)
  50     ensures { sorted a }
  51     ensures { permut_all (old a) a }
  52   = let is_sorted = ref false in
  53     while not !is_sorted do
  54       invariant { permut_all (old a) a }
  55       invariant { !is_sorted -> sorted a }
  56       variant   { (if !is_sorted then 0 else 1), inversions a }
  57       is_sorted := true;
  58       let i = ref 1 in
  59       let ghost half_i = ref 0 in
  60       label L in
  61       while !i < length a - 1 do
  62         invariant { 0 <= !half_i /\ 0 <= !i = 2 * !half_i + 1 }
  63         invariant { permut_all (old a) a }
  64         invariant { odd_sorted a !i }
  65         invariant { if !is_sorted then inversions a = inversions (a at L)
  66                                   else inversions a < inversions (a at L) }
  67         variant   { length a - !i }
  68         if a[!i] > a[!i+1] then begin
  69           swap a !i (!i+1);
  70           is_sorted := false;
  71         end;
  72         i := !i + 2;
  73         ghost half_i := !half_i + 1
  74       done;
  75       assert { odd_sorted a (length a) };
  76       i := 0;
  77       ghost half_i := 0;
  78       while !i < length a - 1 do
  79         invariant { 0 <= !half_i /\ 0 <= !i = 2 * !half_i }
  80         invariant { 0 <= !i }
  81         invariant { permut_all (old a) a }
  82         invariant { !is_sorted -> odd_sorted a (length a) }
  83         invariant { even_sorted a !i }
  84         invariant { if !is_sorted then inversions a = inversions (a at L)
  85                                   else inversions a < inversions (a at L) }
  86         invariant { !is_sorted \/ inversions a < inversions (a at L) }
  87         variant   { length a - !i }
  88         if a[!i] > a[!i+1] then begin
  89           swap a !i (!i+1);
  90           is_sorted := false;
  91         end;
  92         i := !i + 2;
  93         ghost half_i := !half_i + 1
  94       done;
  95       assert { !is_sorted -> even_sorted a (length a) }
  96     done
  97
  98 end