From 93c31d55048958717b53a161c404279d47a42d81 Mon Sep 17 00:00:00 2001 From: Jean-Christophe Filliatre Date: Mon, 20 Jun 2011 09:28:21 +0200 Subject: [PATCH] insertion sort (in progress) --- examples/programs/insertion_sort.mlw | 42 ++++++++++++++++++++++++++++ modules/array.mlw | 3 +- 2 files changed, 44 insertions(+), 1 deletion(-) create mode 100644 examples/programs/insertion_sort.mlw diff --git a/examples/programs/insertion_sort.mlw b/examples/programs/insertion_sort.mlw new file mode 100644 index 000000000..599c7067f --- /dev/null +++ b/examples/programs/insertion_sort.mlw @@ -0,0 +1,42 @@ + +(* Insertion sort. *) + +module InsertionSort + + 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 insertion_sort (a: array int) = + { } + label L: + for i = 1 to length a - 1 do + (* a[0..i[ is sorted; now insert a[i] *) + invariant { sorted_sub a 0 i and permut a (at a L) } + let v = a[i] in + let j = ref i in + while !j > 0 && a[!j - 1] > v do + invariant { + 0 <= !j <= i and permut a[!j <- v] (at a L) and + (forall k1 k2: int. + 0 <= k1 <= k2 <= i -> k1 <> !j -> k2 <> !j -> a[k1] <= a[k2]) and + (forall k: int. !j+1 <= k <= i -> v < a[k]) } + variant { !j } + a[!j] <- a[!j - 1]; + j := !j - 1 + done; + a[!j] <- v + done + { sorted a and permut a (old a) } + +end + +(* +Local Variables: +compile-command: "unset LANG; make -C ../.. examples/programs/insertion_sort.gui" +End: +*) + diff --git a/modules/array.mlw b/modules/array.mlw index 8df59d2d7..88404166a 100644 --- a/modules/array.mlw +++ b/modules/array.mlw @@ -106,8 +106,9 @@ end module ArraySorted + use import int.Int use import module Array - clone import map.MapSorted as M with type elt = int + clone import map.MapSorted as M with type elt = int, logic le = (<=) logic sorted_sub (a : array int) (l u : int) = M.sorted_sub a.elts l u -- GitLab