examples/verifythis_2017_odd_even_sort_rearranging.mlw

   1 use map.Map
   2 use array.Array
   3 use array.IntArraySorted
   4 use array.ArrayPermut
   5 use array.ArraySwap
   6 use int.Int
   7 use ref.Refint
   8 use int.Sum
   9 use number.Parity
  10
  11 let ghost function array_max (a:array int) : int
  12   ensures  { forall j. 0 <= j < length a -> a[j] <= result }
  13 = if length a = 0 then 0
  14   else
  15   let m = ref a[0] in
  16   let i = ref 0 in
  17   while !i < length a do
  18     variant   { length a - !i }
  19     invariant { 0 <= !i <= length a }
  20     invariant { forall j. 0 <= j < !i -> a[j] <= !m }
  21     if a[!i] > !m then m := a[!i];
  22     incr i
  23   done;
  24   !m
  25
  26 function aux (a:int -> int) (m i:int) : int = i * (m - Map.get a i)
  27
  28 lemma aux_pos :
  29   forall a m i. 0 <= i < length a -> a[i] <= m -> aux a.elts m i >= 0
  30
  31 function entropy (a:array int) (m:int) : int = sum (aux a.elts m) 0 (length a)
  32
  33 let rec lemma entropy_pos (a:array int) (m i:int)
  34   requires { 0 <= i <= length a }
  35   requires { forall j. 0 <= j < i <= length a -> a[j] <= m }
  36   ensures { sum (aux a.elts m) 0 i >= 0 }
  37   variant { i }
  38 =
  39   if i > 0
  40   then begin
  41        entropy_pos a m (i-1);
  42        assert { aux a.elts m (i-1) >= 0 };
  43        assert { sum (aux a.elts m) 0 i
  44                 = sum (aux a.elts m) 0 (i-1) + aux a.elts m (i-1) };
  45        end
  46   else ()
  47
  48 let lemma decompose_entropy (a:int -> int) (i j m n:int)
  49   requires { 0 <= i < j < n }
  50   ensures  { sum (aux a m) 0 n
  51              = sum (aux a m) 0 i + sum (aux a m) (j+1) n
  52                + sum (aux a m) (i+1) j + aux a m i + aux a m j }
  53 =  let decomp (i j k: int)
  54      requires { 0 <= i <= j <= k <= n }
  55      ensures  { sum (aux a m) i k = sum (aux a m) i j + sum (aux a m) j k }
  56    = () in
  57    decomp 0 i n; decomp i (j+1) n; decomp i j (j+1); decomp i (i+1) j
  58
  59 let lemma inst_ext (a1 a2: int -> int) (a b m:int)
  60   requires { forall i. a <= i < b -> Map.get a1 i = Map.get a2 i }
  61   ensures { sum (aux a1 m) a b = sum (aux a2 m) a b }
  62 = assert { forall i. a <= i < b -> (aux a1 m) i = (aux a2 m) i }
  63
  64 let my_swap (a:array int) (i j:int) (ghost m:int)
  65   requires { a[i] > a[j] }
  66   requires { 0 <= i < j < length a }
  67   writes   { a }
  68   ensures  { exchange (old a) a i j }
  69   ensures  { entropy a m < entropy (old a) m }
  70 = let ghost a1 = a.elts in
  71   decompose_entropy a1 i j m a.length;
  72   swap a i j;
  73   let ghost a2 = a.elts in
  74   assert { a[i] * i + a[j] * j > a[i] * j + a[j] * i
  75            by a[j] - a[i] > 0 /\ j - i > 0
  76            so a[i] * i + a[j] * j - (a[i] * j + a[j] * i)
  77               = (a[j] - a[i]) * (j-i)
  78               > 0 };
  79   decompose_entropy a2 i j m a.length;
  80   assert { aux a2 m i + aux a2 m j < aux a1 m i + aux a1 m j
  81            by (old a)[i] = a[j]
  82            so (old a)[j] = a[i]
  83            so aux a2 m i + aux a2 m j
  84               = (m - a[i]) * i + (m - a[j]) * j
  85               = m * (i+j) - (a[i] * i + a[j] * j)
  86               < m * (i+j) - (a[i] * j + a[j] * i)
  87               = (m - a[j]) * i + (m - a[i]) * j
  88               = aux a1 m i + aux a1 m j
  89            };
  90   inst_ext a1 a2 0 i m; inst_ext a1 a2 (i+1) j m; inst_ext a1 a2 (j+1) a.length m
  91
  92 let rec lemma local_order_implies_sort_sub (a:array int) (i j:int)
  93   requires { forall k. i <= k < j - 1 -> a[k] <= a[k+1] }
  94   requires { 0 <= i <= j <= length a }
  95   ensures  { sorted_sub a i j }
  96   variant  { j - i }
  97 = if i < j - 1
  98   then begin
  99     local_order_implies_sort_sub a (i+1) j;
 100     assert { forall k l. i <= k <= l < j -> a[k] <= a[l]
 101              by k = l \/  i = k < l \/  i+1 <= k < j };
 102     end
 103
 104 let odd_even_sort (a: array int)
 105     requires { length a > 0 }
 106     ensures  { sorted a }
 107     ensures  { permut_all (old a) a }
 108 =
 109   let ghost m = array_max a in
 110   let ok = ref false in
 111   while not !ok do
 112     variant   { entropy a m + (if !ok then 0 else 1) }
 113     invariant { permut_all (old a) a }
 114     invariant { !ok -> sorted a }
 115     ok := true;
 116     label L in
 117     let i = ref 1 in
 118     while !i < length a - 1 do
 119       variant   { length a - !i }
 120       invariant { permut_all (old a) a }
 121       invariant { 0 <= !i <= length a }
 122       invariant { odd !i }
 123       invariant { !ok -> entropy a m = entropy (a at L) m }
 124       invariant { !ok -> forall j. 0 <= j < !i -> odd j
 125                       -> a[j] <= a[j+1] }
 126       invariant { not !ok -> entropy a m < entropy (a at L) m }
 127       if a[!i] > a[!i+1]
 128       then begin my_swap a !i (!i+1) m; ok := false end;
 129       i := !i + 2
 130     done;
 131     let i = ref 0 in
 132     while !i < length a - 1 do
 133       variant   { length a - !i }
 134       invariant { permut_all (old a) a }
 135       invariant { 0 <= !i <= length a }
 136       invariant { even !i }
 137       invariant { !ok -> entropy a m = entropy (a at L) m }
 138       invariant { !ok -> forall j. 0 <= j < length a - 1 /\ odd j
 139                       -> a[j] <= a[j+1] }
 140       invariant { !ok -> forall j. 0 <= j < !i /\ even j
 141                       -> a[j] <= a[j+1] }
 142       invariant { not !ok -> entropy a m < entropy (a at L) m }
 143       if a[!i] > a[!i+1]
 144       then begin my_swap a !i (!i+1) m; ok := false end;
 145       i := !i + 2
 146     done;
 147   done;