examples/gnome_sort.mlw

   1
   2 (* Gnome sort
   3    https://en.wikipedia.org/wiki/Gnome_sort
   4 *)
   5
   6 module GnomeSort
   7
   8   use int.Int
   9   use ref.Refint
  10   use array.Array
  11   use array.ArrayPermut
  12   use array.IntArraySorted
  13   use array.ArraySwap
  14   use array.Inversions
  15
  16   let gnome_sort (a: array int) : unit
  17     ensures { sorted a }
  18     ensures { permut_all (old a) a }
  19   = let ref pos = 0 in
  20     while pos < length a do
  21       invariant { 0 <= pos <= length a }
  22       invariant { sorted_sub a 0 pos }
  23       invariant { permut_all (old a) a }
  24       variant   { inversions a, length a - pos }
  25       if pos = 0 || a[pos] >= a[pos - 1] then
  26         incr pos
  27       else begin
  28         swap a pos (pos - 1);
  29         decr pos
  30       end
  31     done
  32
  33 end