selection_sort.mlw 1.15 KB
 Jean-Christophe Filliâtre committed Jun 20, 2011 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 `````` (* Selectino sort. *) module Quicksort use import int.Int use import module ref.Ref use import module array.Array use import module array.ArraySorted use import module array.ArrayPermut use import module array.ArrayEq let swap (a: array int) (i: int) (j: int) = { 0 <= i < length a and 0 <= j < length a } let v = a[i] in a[i] <- a[j]; a[j] <- v { exchange a (old a) i j } let selection_sort (a: array int) = { } label L: for i = 0 to length a - 1 do (* a[0..i[ is sorted; now find minimum of a[i..n[ *) invariant { sorted_sub a 0 i and permut a (at a L) and forall k1 k2: int. 0 <= k1 < i <= k2 < length a -> a[k1] <= a[k2] } let min = ref i in for j = i + 1 to length a - 1 do invariant { i <= !min < j && forall k: int. i <= k < j -> a[!min] <= a[k] } if a[j] < a[!min] then min := j done; `````` Jean-Christophe Filliâtre committed Jun 20, 2011 34 35 36 `````` label L1: if !min <> i then swap a !min i; assert { permut a (at a L1) } `````` Jean-Christophe Filliâtre committed Jun 20, 2011 37 38 39 40 41 42 43 44 45 46 47 `````` done { sorted a and permut a (old a) } end (* Local Variables: compile-command: "unset LANG; make -C ../.. examples/programs/selection_sort.gui" End: *) ``````