## 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 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 { 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

Obligations | Alt-Ergo 2.0.0 | Z3 4.6.0 | |

VC for gnome_sort | --- | --- | |

split_goal_right | |||

loop invariant init | 0.01 | --- | |

loop invariant init | 0.00 | --- | |

loop invariant init | 0.01 | --- | |

index in array bounds | 0.01 | --- | |

index in array bounds | 0.01 | --- | |

loop variant decrease | --- | 0.08 | |

loop invariant preservation | 0.01 | --- | |

loop invariant preservation | 0.02 | --- | |

loop invariant preservation | 0.01 | --- | |

precondition | 0.01 | --- | |

loop variant decrease | --- | 0.13 | |

loop invariant preservation | 0.01 | --- | |

loop invariant preservation | 0.02 | --- | |

loop invariant preservation | 0.27 | --- | |

postcondition | 0.01 | --- | |

postcondition | 0.01 | --- |