gnome_sort.mlw 709 Bytes
Newer Older
1 2 3 4 5 6 7

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

module GnomeSort

8 9 10 11 12 13 14
  use int.Int
  use ref.Refint
  use array.Array
  use array.ArrayPermut
  use array.IntArraySorted
  use array.ArraySwap
  use array.Inversions
15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33

  let gnome_sort (a: array int) : unit
    ensures { sorted a }
    ensures { permut_all (old a) a }
  = let pos = ref 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   { 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