examples/insertion_sort.mlw

   1
   2 (** Insertion sort.
   3
   4     Surprinsingly, the verification of insertion sort is more difficult
   5     than the proof of other, more efficient, sorting algorithms.
   6
   7     One reason is that insertion sort proceeds by shifting elements,
   8     which means that, within the inner loop, the array is *not* a permutation
   9     of the initial array. Below we make use of the functional array update
  10     a[j <- v] to state that, if ever we put back `v` at index `j`, we get
  11     an array that is a permutation of the original array.
  12 *)
  13
  14 module InsertionSort
  15
  16   use int.Int
  17   use array.Array
  18   use array.IntArraySorted
  19   use array.ArrayPermut
  20   use array.ArrayEq
  21
  22   let insertion_sort (a: array int) : unit
  23     ensures { sorted a }
  24     ensures { permut_all (old a) a }
  25   = for i = 1 to length a - 1 do
  26       (* a[0..i[ is sorted; now insert a[i] *)
  27       invariant { sorted_sub a 0 i /\ permut_all (old a) a }
  28       let v = a[i] in
  29       let ref j = i in
  30       while j > 0 && a[j - 1] > v do
  31         invariant { 0 <= j <= i }
  32         invariant { permut_all (old a) a[j <- v] }
  33         invariant { forall k1 k2.
  34              0 <= k1 <= k2 <= i -> k1 <> j -> k2 <> j -> a[k1] <= a[k2] }
  35         invariant { forall k. j+1 <= k <= i -> v < a[k] }
  36         variant { j }
  37         label L in
  38         a[j] <- a[j - 1];
  39         assert { exchange (a at L)[j <- v] a[j-1 <- v] (j - 1) j };
  40         j <- j - 1
  41       done;
  42       assert { forall k. 0 <= k < j -> a[k] <= v };
  43       a[j] <- v
  44     done
  45
  46   let test1 () =
  47     let a = make 3 0 in
  48     a[0] <- 7; a[1] <- 3; a[2] <- 1;
  49     insertion_sort a;
  50     a
  51
  52   let test2 () ensures { result.length = 8 } =
  53     let a = make 8 0 in
  54     a[0] <- 53; a[1] <- 91; a[2] <- 17; a[3] <- -5;
  55     a[4] <- 413; a[5] <- 42; a[6] <- 69; a[7] <- 6;
  56     insertion_sort a;
  57     a
  58
  59   exception BenchFailure
  60
  61   let bench () raises { BenchFailure -> true } =
  62     let a = test2 () in
  63     if a[0] <> -5 then raise BenchFailure;
  64     if a[1] <> 6 then raise BenchFailure;
  65     if a[2] <> 17 then raise BenchFailure;
  66     if a[3] <> 42 then raise BenchFailure;
  67     if a[4] <> 53 then raise BenchFailure;
  68     if a[5] <> 69 then raise BenchFailure;
  69     if a[6] <> 91 then raise BenchFailure;
  70     if a[7] <> 413 then raise BenchFailure;
  71     a
  72
  73 end
  74
  75 module InsertionSortGen
  76
  77   use int.Int
  78   use array.Array
  79   use array.ArrayPermut
  80   use array.ArrayEq
  81
  82   type elt
  83
  84   val predicate le elt elt
  85
  86   clone map.MapSorted as M with type elt = elt, predicate le = le
  87
  88   axiom le_refl: forall x:elt. le x x
  89
  90   axiom le_asym: forall x y:elt. not (le x y) -> le y x
  91
  92   axiom le_trans: forall x y z:elt. le x y /\ le y z -> le x z
  93
  94   predicate sorted_sub (a : array elt) (l u : int) =
  95     M.sorted_sub a.elts l u
  96
  97   predicate sorted (a : array elt) =
  98     M.sorted_sub a.elts 0 a.length
  99
 100   let insertion_sort (a: array elt) : unit
 101     ensures { sorted a }
 102     ensures { permut_all (old a) a }
 103   = for i = 1 to length a - 1 do
 104       (* a[0..i[ is sorted; now insert a[i] *)
 105       invariant { sorted_sub a 0 i }
 106       invariant { permut_all (old a) a }
 107       let v = a[i] in
 108       let ref j = i in
 109       while j > 0 && not (le a[j - 1] v) do
 110         invariant { 0 <= j <= i }
 111         invariant { permut_all (old a) a[j <- v] }
 112         invariant { forall k1 k2.
 113              0 <= k1 <= k2 <= i -> k1 <> j -> k2 <> j -> le a[k1] a[k2] }
 114         invariant { forall k. j+1 <= k <= i -> le v a[k] }
 115         variant { j }
 116         label L in
 117         a[j] <- a[j - 1];
 118         assert { exchange (a at L)[j <- v] a[j-1 <- v] (j - 1) j };
 119         j <- j - 1
 120       done;
 121       assert { forall k. 0 <= k < j -> le a[k] v };
 122       a[j] <- v
 123     done
 124
 125 end
 126
 127 (** Using swaps (instead of shifting) is less efficient but at least
 128     we can expect the loop invariant for the inner loop to be
 129     simpler. And indeed it is.
 130
 131     The invariant below was suggested by Xavier Leroy (Collège de France).
 132
 133     Without surprise, the proof of the permutation property is also simpler.
 134 *)
 135
 136 module InsertionSortSwaps
 137
 138   use int.Int
 139   use array.Array
 140   use array.ArraySwap
 141   use array.ArrayPermut
 142
 143   let insertion_sort (a: array int) : unit
 144     ensures { forall p q. 0 <= p <= q < length a -> a[p] <= a[q] }
 145     ensures { permut_all (old a) a }
 146   = for i = 1 to length a - 1 do
 147       invariant { forall p q. 0 <= p <= q < i -> a[p] <= a[q] }
 148       invariant { permut_all (old a) a }
 149       let ref j = i in
 150       while j > 0 && a[j - 1] > a[j] do
 151         invariant { 0 <= j <= i }
 152         invariant { permut_all (old a) a }
 153         invariant { forall p q. 0 <= p <= q <= i -> q <> j -> a[p] <= a[q] }
 154         variant   { j }
 155         swap a (j - 1) j;
 156         j <- j - 1
 157       done
 158     done
 159
 160 end