why3/examples/gnome_sort.mlw

(* Gnome sort
   https://en.wikipedia.org/wiki/Gnome_sort
*)

module GnomeSort

  use int.Int
  use ref.Refint
  use array.Array
  use array.ArrayPermut
  use array.IntArraySorted
  use array.ArraySwap
  use array.Inversions

  let gnome_sort (a: array int) : unit
    ensures { sorted a }
    ensures { permut_all (old a) a }
  = let ref pos = 0 in
    while pos < length a do
      invariant { 0 <= pos <= length a }
      invariant { sorted_sub a 0 pos }
      invariant { permut_all (old a) a }
      variant   { 2 * inversions a + length a - pos }
      if pos = 0 || a[pos] >= a[pos - 1] then
        incr pos
      else begin
        swap a pos (pos - 1);
        decr pos
      end
    done

end