why3/examples/insertion_sort.mlw

(** Insertion sort.

    Surprinsingly, the verification of insertion sort is more difficult
    than the proof of other, more efficient, sorting algorithms.

    One reason is that insertion sort proceeds by shifting elements,
    which means that, within the inner loop, the array is *not* a permutation
    of the initial array. Below we make use of the functional array update
    a[j <- v] to state that, if ever we put back `v` at index `j`, we get
    an array that is a permutation of the original array.
*)

module InsertionSort

  use int.Int
  use array.Array
  use array.IntArraySorted
  use array.ArrayPermut
  use array.ArrayEq

  let insertion_sort (a: array int) : unit
    ensures { sorted a }
    ensures { permut_all (old a) a }
  = for i = 1 to length a - 1 do
      (* a[0..i[ is sorted; now insert a[i] *)
      invariant { sorted_sub a 0 i /\ permut_all (old a) a }
      let v = a[i] in
      let ref j = i in
      while j > 0 && a[j - 1] > v do
        invariant { 0 <= j <= i }
        invariant { permut_all (old a) a[j <- v] }
        invariant { forall k1 k2.
             0 <= k1 <= k2 <= i -> k1 <> j -> k2 <> j -> a[k1] <= a[k2] }
        invariant { forall k. j+1 <= k <= i -> v < a[k] }
        variant { j }
        label L in
        a[j] <- a[j - 1];
        assert { exchange (a at L)[j <- v] a[j-1 <- v] (j - 1) j };
        j <- j - 1
      done;
      assert { forall k. 0 <= k < j -> a[k] <= v };
      a[j] <- v
    done

  let test1 () =
    let a = make 3 0 in
    a[0] <- 7; a[1] <- 3; a[2] <- 1;
    insertion_sort a;
    a

  let test2 () ensures { result.length = 8 } =
    let a = make 8 0 in
    a[0] <- 53; a[1] <- 91; a[2] <- 17; a[3] <- -5;
    a[4] <- 413; a[5] <- 42; a[6] <- 69; a[7] <- 6;
    insertion_sort a;
    a

  exception BenchFailure

  let bench () raises { BenchFailure -> true } =
    let a = test2 () in
    if a[0] <> -5 then raise BenchFailure;
    if a[1] <> 6 then raise BenchFailure;
    if a[2] <> 17 then raise BenchFailure;
    if a[3] <> 42 then raise BenchFailure;
    if a[4] <> 53 then raise BenchFailure;
    if a[5] <> 69 then raise BenchFailure;
    if a[6] <> 91 then raise BenchFailure;
    if a[7] <> 413 then raise BenchFailure;
    a

end

module InsertionSortGen

  use int.Int
  use array.Array
  use array.ArrayPermut
  use array.ArrayEq

  type elt

  val predicate le elt elt

  clone map.MapSorted as M with type elt = elt, predicate le = le

  axiom le_refl: forall x:elt. le x x

  axiom le_asym: forall x y:elt. not (le x y) -> le y x

  axiom le_trans: forall x y z:elt. le x y /\ le y z -> le x z

  predicate sorted_sub (a : array elt) (l u : int) =
    M.sorted_sub a.elts l u

  predicate sorted (a : array elt) =
    M.sorted_sub a.elts 0 a.length

  let insertion_sort (a: array elt) : unit
    ensures { sorted a }
    ensures { permut_all (old a) a }
  = for i = 1 to length a - 1 do
      (* a[0..i[ is sorted; now insert a[i] *)
      invariant { sorted_sub a 0 i }
      invariant { permut_all (old a) a }
      let v = a[i] in
      let ref j = i in
      while j > 0 && not (le a[j - 1] v) do
        invariant { 0 <= j <= i }
        invariant { permut_all (old a) a[j <- v] }
        invariant { forall k1 k2.
             0 <= k1 <= k2 <= i -> k1 <> j -> k2 <> j -> le a[k1] a[k2] }
        invariant { forall k. j+1 <= k <= i -> le v a[k] }
        variant { j }
        label L in
        a[j] <- a[j - 1];
        assert { exchange (a at L)[j <- v] a[j-1 <- v] (j - 1) j };
        j <- j - 1
      done;
      assert { forall k. 0 <= k < j -> le a[k] v };
      a[j] <- v
    done

end

(** Using swaps (instead of shifting) is less efficient but at least
    we can expect the loop invariant for the inner loop to be
    simpler. And indeed it is.

    The invariant below was suggested by Xavier Leroy (Collège de France).

    Without surprise, the proof of the permutation property is also simpler.
*)

module InsertionSortSwaps

  use int.Int
  use array.Array
  use array.ArraySwap
  use array.ArrayPermut

  let insertion_sort (a: array int) : unit
    ensures { forall p q. 0 <= p <= q < length a -> a[p] <= a[q] }
    ensures { permut_all (old a) a }
  = for i = 1 to length a - 1 do
      invariant { forall p q. 0 <= p <= q < i -> a[p] <= a[q] }
      invariant { permut_all (old a) a }
      let ref j = i in
      while j > 0 && a[j - 1] > a[j] do
        invariant { 0 <= j <= i }
        invariant { permut_all (old a) a }
        invariant { forall p q. 0 <= p <= q <= i -> q <> j -> a[p] <= a[q] }
        variant   { j }
        swap a (j - 1) j;
        j <- j - 1
      done
    done

end