## Gnome Sort

A simple sort algorithm using a single loop

Authors: Jean-Christophe Filliâtre

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
```

# Why3 Proof Results for Project "gnome_sort"

## Theory "gnome_sort.GnomeSort": fully verified

 Obligations Alt-Ergo 2.0.0 Z3 4.6.0 VC gnome_sort --- --- split_goal_right VC gnome_sort.0 0.01 --- VC gnome_sort.1 0.00 --- VC gnome_sort.2 0.01 --- VC gnome_sort.3 0.01 --- VC gnome_sort.4 0.01 --- VC gnome_sort.5 --- 0.08 VC gnome_sort.6 0.01 --- VC gnome_sort.7 0.02 --- VC gnome_sort.8 0.01 --- VC gnome_sort.9 0.01 --- VC gnome_sort.10 --- 0.13 VC gnome_sort.11 0.01 --- VC gnome_sort.12 0.02 --- VC gnome_sort.13 0.27 --- VC gnome_sort.14 0.01 --- VC gnome_sort.15 0.01 ---