Wiki Agenda Contact Version française

Gnome Sort

A simple sort algorithm using a single loop


Authors: Jean-Christophe Filliâtre

Topics: Array Data Structure / Algorithms / Sorting Algorithms

Tools: Why3

see also the index (by topic, by tool, by reference, by year)


(* 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 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

download ZIP archive

Why3 Proof Results for Project "gnome_sort"

Theory "gnome_sort.GnomeSort": fully verified

ObligationsAlt-Ergo 1.30Z3 4.4.0
VC gnome_sort------
split_goal_right
VC gnome_sort.00.01---
VC gnome_sort.10.00---
VC gnome_sort.20.01---
VC gnome_sort.30.01---
VC gnome_sort.40.01---
VC gnome_sort.5---0.08
VC gnome_sort.60.01---
VC gnome_sort.70.02---
VC gnome_sort.80.01---
VC gnome_sort.90.01---
VC gnome_sort.10---0.13
VC gnome_sort.110.01---
VC gnome_sort.120.02---
VC gnome_sort.130.05---
VC gnome_sort.140.01---
VC gnome_sort.150.01---