Contact Version française

The ProVal team was stopped at the end of August 2012, and reborn into a new team Toccata
These pages do not evolve anymore, please follow the link above for up-to-date informations about our team.

Insertion sort (arrays)

Sorting an array of integers using insertion sort.

Authors: Jean-Christophe Filliâtre

Topics: Array Data Structure / Sorting Algorithm

Tools: Why3

index 


(* Insertion sort. *)

module InsertionSort

  use import int.Int
  use import ref.Ref
  use import array.Array
  use import array.ArraySorted
  use import array.ArrayPermut
  use import array.ArrayEq

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

end
download ZIP archive